nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

Quantifier-Free Equational Logic and Prime Implicate Generation

verfasst von : Mnacho Echenim, Nicolas Peltier, Sophie Tourret

Erschienen in: Automated Deduction - CADE-25

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

An algorithm for generating prime implicates of sets of equational ground clauses is presented. It consists in extending the standard Superposition Calculus with rules that allow attaching hypotheses to clauses to perform additional inferences. The hypotheses that lead to a refutation represent implicates of the original set of clauses. The set of prime implicates of a clausal set can thus be obtained by saturation of this set. Data structures and algorithms are also devised to represent sets of constrained clauses in an efficient and concise way.

Our method is proven to be correct and complete. Practical experimentations show the relevance of our method in comparison to existing approaches for propositional or first-order logic.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel CTL Model Checking in Deduction Modulo

Nächstes Kapitel Quantomatic: A Proof Assistant for Diagrammatic Reasoning

Using logical entailment makes the calculus incomplete due to the deletion of clauses whose constraint is not in normal form.

Many thanks to Prof. L. Simon for providing the executable file.

Many thanks to Prof. H. Nabeshima for providing the executable file.

Personal communication of Prof. Nabeshima.

http://users.cecs.anu.edu.au/~baumgart/systems/smttotptp/.

Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 1–51 (2009)MathSciNetCrossRef

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa (2010). www.SMT-LIB.org

Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symb. Comput. 45(2), 229–260 (2010)MathSciNetCrossRefMATH

Cruanes, S.:. Logtk: A logic ToolKit for automated reasoning and its implementation. In: 4th Workshop on Practical Aspects of Automated Reasoning (2014)

De Kleer, J.: An improved incremental algorithm for generating prime implicates. In: Proceedings of the National Conference on Artificial Intelligence, p. 780. Wiley (1992)

Dershowitz, N.: Orderings for term-rewriting systems. In: Proceedings of the 20th Annual Symposium on Foundations of Computer Science, pp. 123–131. IEEE Computer Society, Washington (1979)

Dillig, I., Dillig, T., McMillan, K.L., Aiken, A.: Minimum satisfying assignments for SMT. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 394–409. Springer, Heidelberg (2012) CrossRef

Echenim, M., Peltier, N., Tourret, S.: An approach to abductive reasoning in equational logic. In: Rossi, F. (ed.) IJCAI 2013 - International Joint Conference on Artificial Intelligence, pp. 531–537. AAAI Press, Beijing, August 2013

10.

Echenim, M., Peltier, N., Tourret, S.: A rewriting strategy to generate prime implicates in equational logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 137–151. Springer, Heidelberg (2014)

11.

Iwanuma, K., Nabeshima, H., Inoue.: Toward an efficient equality computation in connection tableaux: A modification method without symmetry transformation—a preliminary report . First-Order Theorem Proving, p. 19 (2009)

12.

Jackson, P.: Computing prime implicates incrementally. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)

13.

Kean, A., Tsiknis, G.: An incremental method for generating prime implicants/implicates. J. Symb. Comput. 9(2), 185–206 (1990)MathSciNetCrossRefMATH

14.

Knill, E., Cox, P.T., Pietrzykowski, T.: Equality and abductive residua for horn clauses. Theoret. Comput. Sci. 120(1), 1–44 (1993)MathSciNetCrossRefMATH

15.

Marquis, P.: Extending abduction from propositional to first-order logic. In: Jorrand, P., Kelemen, J. (eds.) FAIR 1991. LNCS, vol. 535. Springer, Heidelberg (1991) CrossRef

16.

Matusiewicz, A., Murray, N.V., Rosenthal, E.: Prime implicate tries. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 250–264. Springer, Heidelberg (2009) CrossRef

17.

Matusiewicz, A., Murray, N.V., Rosenthal, E.: Tri-based set operations and selective computation of prime implicates. In: Kryszkiewicz, M., Rybinski, H., Skowron, A., Raś, Z.W. (eds.) ISMIS 2011. LNCS, vol. 6804, pp. 203–213. Springer, Heidelberg (2011) CrossRef

18.

Mayer, M.C., Pirri, F.: First order abduction via tableau and sequent calculi. Log. J. IGPL 1(1), 99–117 (1993)CrossRefMATH

19.

Nabeshima, H., Iwanuma, K., Inoue, K., Ray, O.: SOLAR: an automated deduction system for consequence finding. AI Commun. 23(2), 183–203 (2010)MathSciNetMATH

20.

Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371–443. North Holland, Amsterdam (2001)CrossRef

21.

Schmidt-Schauss, M.: Implication of clauses is undecidable. Theor. Comput. Sci. 59, 287–296 (1988)MathSciNetCrossRefMATH

22.

Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2–3), 111–126 (2002)MATH

23.

Schulz, S.: System Description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013) CrossRef

24.

Simon, L., Del Val A.: Efficient consequence finding. In: International Joint Conference on Artificial Intelligence, vol. 17, pp. 359–370. Lawrence Erlbaum Associates ltd (2001)

25.

Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)CrossRefMATH

26.

Tison, P.: Generalization of consensus theory and application to the minimization of boolean functions. IEEE Trans. Electron. Comput. EC–16(4), 446–456 (1967)CrossRef

Titel: Quantifier-Free Equational Logic and Prime Implicate Generation
verfasst von: Mnacho Echenim
Nicolas Peltier
Sophie Tourret
Verlag: Springer International Publishing
Buch: Automated Deduction - CADE-25
Print ISBN: 978-3-319-21400-9

Electronic ISBN: 978-3-319-21401-6

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-319-21401-6_21

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"