Unfolding Existentially Quantified Sets of Extended Clauses

Kiyoshi Akama, Ekawit Nantajeewarawat

2016

Abstract

Conventional theories cannot solve many logical problems due to the limitations of the underlying clause space. In conventional clauses, all variables are universally quantified and no existential quantification is allowed. Conventional clauses are therefore not sufficiently expressive for representing first-order formulas. To extend clauses with the expressive power of existential quantification, variables of a new type, called function variables, have been introduced, resulting in a new space of extended clauses, called ECLS_F. This new space is necessary to overcome the limitations of the conventional clause space. To solve problems on ECLS_F, many equivalent transformation rules are used. We formally defined unfolding transformation on ECLS_F, which is applicable not only to definite clauses but also to multi-head clauses. The proposed unfolding transformation preserves the answers to model-intersection problems and is useful for solving many logical problems such as proof problems and query-answering problems on first-order logic with built-in constraint atoms.

Paper Citation

in Harvard Style

Akama K. and Nantajeewarawat E. (2016). Unfolding Existentially Quantified Sets of Extended Clauses . 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 96-103. DOI: 10.5220/0006051500960103

in Bibtex Style

@conference{keod16,
author={Kiyoshi Akama and Ekawit Nantajeewarawat},
title={Unfolding Existentially Quantified Sets of Extended Clauses},
booktitle={Proceedings of the 8th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management - Volume 2: KEOD, (IC3K 2016)},
year={2016},
pages={96-103},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0006051500960103},
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 - Unfolding Existentially Quantified Sets of Extended Clauses
SN - 978-989-758-203-5
AU - Akama K.
AU - Nantajeewarawat E.
PY - 2016
SP - 96
EP - 103
DO - 10.5220/0006051500960103