| Autor: |
Kiyoshi Akama, Nantajeewarawat, Ekawit |
| Předmět: |
|
| Zdroj: |
Annual International Conference on Network Technologies & Communications; 2012, p87-92, 6p |
| Abstrakt: |
Conversion of a first-order formula into a conjunctive normal form involves removal of existential quantifications by Skolemization. Classical Skolemization, however, does not preserve the logical meaning of a formula. In this paper, we propose an extension of first-order formulas by incorporation of function constants and function variables. By applying function constants to ground arguments, syntactically different extended first-order terms may be evaluated into the same extended term. Extended terms thus constitute a quotient space. The resulting extended formula space allows meaning-preserving Skolemization by converting an existentially quantified usual variable into an extended term with an existentially quantified function variable. A procedure for transforming a first-order formula into an extended conjunctive normal form on the extended space is presented. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
