×

Quantifier-free equational logic and prime implicate generation. (English) Zbl 1465.68280

Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 311-325 (2015).
Summary: 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.
For the entire collection see [Zbl 1316.68011].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Armando, A.; Bonacina, MP; Ranise, S.; Schulz, S., New results on rewrite-based satisfiability procedures, ACM Trans. Comput. Log., 10, 1, 1-51 (2009) · Zbl 1367.68243 · doi:10.1145/1459010.1459014
[2] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge: Cambridge University Press, Cambridge
[3] 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
[4] Bonacina, MP; Echenim, M., Theory decision by decomposition, J. Symb. Comput., 45, 2, 229-260 (2010) · Zbl 1192.68626 · doi:10.1016/j.jsc.2008.10.008
[5] Cruanes, S.:. Logtk: A logic ToolKit for automated reasoning and its implementation. In: 4th Workshop on Practical Aspects of Automated Reasoning (2014)
[6] De Kleer, J.: An improved incremental algorithm for generating prime implicates. In: Proceedings of the National Conference on Artificial Intelligence, p. 780. Wiley (1992) · Zbl 0944.68173
[7] 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)
[8] Dillig, I.; Dillig, T.; McMillan, KL; Aiken, A.; Madhusudan, P.; Seshia, SA, Minimum satisfying assignments for SMT, Computer Aided Verification, 394-409 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-31424-7_30
[9] 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.; Demri, S.; Kapur, D.; Weidenbach, C., A rewriting strategy to generate prime implicates in equational logic, Automated Reasoning, 137-151 (2014), Heidelberg: Springer, Heidelberg · Zbl 1423.68412
[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.; Kapur, D., Computing prime implicates incrementally, Automated Deduction - CADE-11 (1992), Heidelberg: Springer, Heidelberg · Zbl 0925.03054
[13] Kean, A.; Tsiknis, G., An incremental method for generating prime implicants/implicates, J. Symb. Comput., 9, 2, 185-206 (1990) · Zbl 0704.68100 · doi:10.1016/S0747-7171(08)80029-6
[14] Knill, E.; Cox, PT; Pietrzykowski, T., Equality and abductive residua for horn clauses, Theoret. Comput. Sci., 120, 1, 1-44 (1993) · Zbl 0788.68133 · doi:10.1016/0304-3975(93)90243-M
[15] Marquis, P.; Jorrand, P.; Kelemen, J., Extending abduction from propositional to first-order logic, Fundamentals of Artificial Intelligence Research (1991), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-54507-7_12
[16] Matusiewicz, A.; Murray, NV; Rosenthal, E.; Giese, M.; Waaler, A., Prime implicate tries, Automated Reasoning with Analytic Tableaux and Related Methods, 250-264 (2009), Heidelberg: Springer, Heidelberg · Zbl 1260.68127 · doi:10.1007/978-3-642-02716-1_19
[17] Matusiewicz, A.; Murray, NV; Rosenthal, E.; Kryszkiewicz, M.; Rybinski, H.; Skowron, A.; Raś, ZW, Tri-based set operations and selective computation of prime implicates, Foundations of Intelligent Systems, 203-213 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-21916-0_23
[18] Mayer, MC; Pirri, F., First order abduction via tableau and sequent calculi, Log. J. IGPL, 1, 1, 99-117 (1993) · Zbl 0807.03005 · doi:10.1093/jigpal/1.1.99
[19] Nabeshima, H.; Iwanuma, K.; Inoue, K.; Ray, O., SOLAR: an automated deduction system for consequence finding, AI Commun., 23, 2, 183-203 (2010) · Zbl 1205.68362
[20] Nieuwenhuis, R.; Rubio, A.; Robinson, A.; Voronkov, A., Paramodulation-based theorem proving, Handbook of Automated Reasoning, 371-443 (2001), Amsterdam: North Holland, Amsterdam · Zbl 0997.03012 · doi:10.1016/B978-044450813-3/50009-6
[21] Schmidt-Schauss, M., Implication of clauses is undecidable, Theor. Comput. Sci., 59, 287-296 (1988) · Zbl 0657.03006 · doi:10.1016/0304-3975(88)90146-6
[22] Schulz, S., E - a brainiac theorem prover, AI Commun., 15, 2-3, 111-126 (2002) · Zbl 1020.68084
[23] Schulz, S.; McMillan, K.; Middeldorp, A.; Voronkov, A., System Description: E 1.8, Logic for Programming, Artificial Intelligence, and Reasoning, 735-743 (2013), Heidelberg: Springer, Heidelberg · Zbl 1407.68442 · doi:10.1007/978-3-642-45221-5_49
[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) · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8
[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) · Zbl 0158.16102 · doi:10.1109/PGEC.1967.264648
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.