Model-Intersection Problems with Existentially Quantified Function Variables: Formalization and a Solution Schema

Kiyoshi Akama, Ekawit Nantajeewarawat

2016

Abstract

Built-in constraint atoms play a very important role in knowledge representation and are indispensable for practical applications. It is very natural to use built-in constraint atoms together with user-defined atoms when formalizing logical problems using first-order formulas. In the presence of built-in constraint atoms, however, the conventional Skolemization in general preserves neither the satisfiability nor the logical meaning of a given first-order formula, motivating us to step outside the conventional Skolemization and the usual space of first- order formulas. We propose general solutions for proof problems and query-answering (QA) problems on first-order formulas possibly with built-in constraint atoms. We map, by using new meaning-preserving Skolemization, all proof problems and all QA problems, preserving their answers, into a new class of model-intersection (MI) problems on an extended clause space, where clauses are in a sense ``higher-order'' since they may contain not only built-in constraint atoms but also function variables. We propose a general schema for solving this class of MI problems by equivalent transformation (ET), where problems are solved by repeated simplification using ET rules. The correctness of this solution schema is shown. Since MI problems in this paper form a very large class of logical problems, this theory is also useful for inventing solutions for many classes of logical problems.

Paper Citation

in Harvard Style

Akama K. and Nantajeewarawat E. (2016). Model-Intersection Problems with Existentially Quantified Function Variables: Formalization and a Solution Schema . In Proceedings of the 8th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management - Volume 2: KEOD, (IC3K 2016) ISBN 978-989-758-203-5, pages 52-63. DOI: 10.5220/0006056800520063

in Bibtex Style

@conference{keod16,
author={Kiyoshi Akama and Ekawit Nantajeewarawat},
title={Model-Intersection Problems with Existentially Quantified Function Variables: Formalization and a Solution Schema},
booktitle={Proceedings of the 8th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management - Volume 2: KEOD, (IC3K 2016)},
year={2016},
pages={52-63},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0006056800520063},
isbn={978-989-758-203-5},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 8th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management - Volume 2: KEOD, (IC3K 2016)
TI - Model-Intersection Problems with Existentially Quantified Function Variables: Formalization and a Solution Schema
SN - 978-989-758-203-5
AU - Akama K.
AU - Nantajeewarawat E.
PY - 2016
SP - 52
EP - 63
DO - 10.5220/0006056800520063