Translation of first order formulas into ground formulas via a completion theory. (English) Zbl 1436.03100
Summary: A translation technique is presented which transforms a class of First Order Logic formulas, called Restricted formulas, into ground formulas. For the formulas in this class the range of quantified variables is restricted by Domain formulas.
If we have a complete knowledge of the predicates involved in the Domain formulas their extensions can be evaluated with the Relational Algebra and these extensions are used to transform universal (respectively existential) quantifiers into finite conjunctions (respectively disjunctions).
It is assumed that the complete knowledge is represented by Completion Axioms and Unique Name Axioms à la Reiter. These axioms involve the equality predicate. However, the translation allows to remove the equality in the ground formulas and for a large class of formulas their consequences are the same as the initial First Order formulas. This result open the door for the design of efficient deduction techniques.
If we have a complete knowledge of the predicates involved in the Domain formulas their extensions can be evaluated with the Relational Algebra and these extensions are used to transform universal (respectively existential) quantifiers into finite conjunctions (respectively disjunctions).
It is assumed that the complete knowledge is represented by Completion Axioms and Unique Name Axioms à la Reiter. These axioms involve the equality predicate. However, the translation allows to remove the equality in the ground formulas and for a large class of formulas their consequences are the same as the initial First Order formulas. This result open the door for the design of efficient deduction techniques.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68T27 | Logic in artificial intelligence |
| 68V20 | Formalization of mathematics in connection with theorem provers |
Keywords:
modeling in logic; domain; independent formulas; automated deduction; application to biologySoftware:
SOLARReferences:
| [1] | Andréka, H.; Németi, I.; van Bentem, J., Modal languages and bounded fragment of predicate logic, J. Philos. Log., 27, 3 (1998) · Zbl 0919.03013 |
| [2] | Artaud, A.; Nicolas, J-M., An experimental query system: SYNTEX, (Proc. of International Computing Symposium (1974), North-Holland) |
| [3] | (Baldoni, M.; Baroglio, C.; Boella, G.; Micalizio, R., Automated Selection of Grounding Algorithm in Answer Set Programming. Automated Selection of Grounding Algorithm in Answer Set Programming, Lecture Notes in Computer Science, vol. 8249 (2013), Springer) · Zbl 1277.68003 |
| [4] | Bossu, G.; Siegel, P., La saturation au secours de la non-monotonie (1981), Université d’Aix-Marseille: Université d’Aix-Marseille France, PhD thesis |
| [5] | Cooper, E., On the expressive power of query languages for relational databases (1980), Aiken Computation Laboratory, Technical report TR-14-80 |
| [6] | Demolombe, R., Utilisation du Calcul des Prédicats comme langage d’interrogation des Bases de Données (1982), Université Paul Sabatier: Université Paul Sabatier Toulouse, Thèse d’état |
| [7] | Demolombe, R., Syntactical characterization of a subset of domain independent formulas, J. ACM, 39, 1 (1992) · Zbl 0799.68061 |
| [8] | Demolombe, R.; Pozos Parra, M. P., An extension of sol-resolution to theories with equality, (Proceedings of the International Joint Conference on Automated Reasoning (2001)) |
| [9] | Demolombe, R.; Fariñas del Cerro, L.; Obeid, N., A logical model for molecular interaction maps, (Fariñas del Cerro, L.; Inoue, K., Logical Modeling of Biological Systems (2014), Wiley) |
| [10] | Di Paola, R. A., The recursive unsolvability of the decision problem for the class of Definite Formulas, J. ACM, 16, 2 (1969) · Zbl 0182.33202 |
| [11] | Imielinski, T.; Lipski, W., The relational model of data and cylindric algebras (1981), Institute of Computer Science, Polish Academy of Science, Technical report 446 |
| [12] | Inoue, K., Linear resolution for consequence finding, Artif. Intell. Int. J., 56 (1992) · Zbl 0805.68105 |
| [13] | Kohn, K.; Pommier, Y., Molecular interaction map of the p53 and Mdm2 logic elements, which control the Off-On switch of p53 response to DNA damage, Biochem. Biophys. Res. Commun., 331, 3, 816-827 (2005) |
| [14] | Kuhns, J. L., Interrogating a relational data file (1970), Rand Corporation, Technical report R-511-PR |
| [15] | Lifschitz, V., What is answer set programming?, (Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence (2008), AAAI), 1594-1597 |
| [16] | Liu, H.-C.; Yu, J. X.; Liang, W., Safety, domain independence and translation of complex value database queries, Inf. Sci., 178, 2507-2533 (2008) · Zbl 1183.68249 |
| [17] | Manzano, M., Introduction to many-sorted logic, (Meinke, K.; Tucker, J. V., Many-Sorted Logic and Its Applications (1993), ACM Digital Library) |
| [18] | Nabeshima, H.; Iwanuma, K.; Inoue, K.; Ray, O., SOLAR: an automated deduction system for consequence finding, AI Commun., 23, 2-3, 183-203 (2010) · Zbl 1205.68362 |
| [19] | Nicolas, J.-M., Logic for improving integrity checking in relational data bases, Acta Inform., 18, 3 (1982) · Zbl 0478.68096 |
| [20] | Obeid, N., MIM-logic: a logic for reasoning about molecular interaction maps (2014), Université de Toulouse Paul Sabatier, PhD thesis |
| [21] | Pommier, Y.; Weinstein, J.; Aladjem, M.; Kohn, K., Chk2 molecular interaction map and rationale for Chk2 inhibitors, Clin. Cancer Res., 12, 9, 2657-2661 (2006) |
| [22] | Topor, R. W., Domain-independent formulas and databases, Theor. Comput. Sci., 52, 3, 281-306 (1987) · Zbl 0627.68077 |
| [23] | Ullman, J. D., Principles of Database Systems (1980), Computer Science Press · Zbl 0416.68086 |
| [24] | Van Gelder, A.; Topor, R., Safety and translation of relational calculus queries, ACM Trans. Database Syst., 16, 2, 235-278 (1991) |
| [25] | Walther, C., A mechanical solution of Schubert’s steamroller by many-sorted resolution, Artif. Intell., 26, 2 (1985) · Zbl 0569.68076 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
