MEANING-PRESERVING SKOLEMIZATION

Kiyoshi Akama, Ekawit Nantajeewarawat

2011

Abstract

Skolemization is a well-known method for removing existential quantifiers from a logical formula. Although it always yields a satisfiability-preserving transformation step, classical Skolemization in general does not preserve the logical meaning of a source formula. We develop in this paper a theory for extending a space of logical formulas by incorporation of function variables and show how meaning-preserving Skolemization can be achieved in an obtained extended space. A procedure for converting a logical formula into an equivalent one in an extended conjunctive normal form on the extended space is described. This work lays a theoretical foundation for solving logical problems involving existential quantifications based on meaning-preserving formula transformation.

Paper Citation

in Harvard Style

Akama K. and Nantajeewarawat E. (2011). MEANING-PRESERVING SKOLEMIZATION . In Proceedings of the International Conference on Knowledge Engineering and Ontology Development - Volume 1: KEOD, (IC3K 2011) ISBN 978-989-8425-80-5, pages 322-327. DOI: 10.5220/0003692003220327

in Bibtex Style

@conference{keod11,
author={Kiyoshi Akama and Ekawit Nantajeewarawat},
title={MEANING-PRESERVING SKOLEMIZATION},
booktitle={Proceedings of the International Conference on Knowledge Engineering and Ontology Development - Volume 1: KEOD, (IC3K 2011)},
year={2011},
pages={322-327},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0003692003220327},
isbn={978-989-8425-80-5},
}

in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Knowledge Engineering and Ontology Development - Volume 1: KEOD, (IC3K 2011)
TI - MEANING-PRESERVING SKOLEMIZATION
SN - 978-989-8425-80-5
AU - Akama K.
AU - Nantajeewarawat E.
PY - 2011
SP - 322
EP - 327
DO - 10.5220/0003692003220327