Top

Published in:

2018 | OriginalPaper | Chapter

A Generic Framework for Implicate Generation Modulo Theories

Authors : Mnacho Echenim, Nicolas Peltier, Yanis Sellami

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The clausal logical consequences of a formula are called its implicates. The generation of these implicates has several applications, such as the identification of missing hypotheses in a logical specification. We present a procedure that generates the implicates of a quantifier-free formula modulo a theory. No assumption is made on the considered theory, other than the existence of a decision procedure. The algorithm has been implemented (using the solvers MiniSAT, CVC4 and Z3) and experimental results show evidence of the practical relevance of the proposed approach.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Complexity of Combinations of Qualitative Constraint Satisfaction Problems

next chapter A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems

Note that this ordering is not necessarily related to the ordering \(\prec \) on clauses.

A refined comparison of the set of generated \((\mathcal{T},\mathcal{A})\)-implicates modulo theory entailment is left for future work.

Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14CrossRef

Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). www.SMT-LIB.org

Bienvenu, M.: Prime implicates and prime implicants in modal logic. In: Proceedings of the National Conference on Artificial Intelligence, vol. 22, p. 379. AAAI Press/MIT Press, Menlo Park, Cambridge, London (1999, 2007)

Blackburn, P., Van Benthem, J., Wolter, F.: Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier, Amsterdam (2007). ISSN 1570–2464MATH

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

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

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). https://doi.org/10.1007/978-3-642-31424-7_30CrossRef

Echenim, M., Peltier, N.: A superposition calculus for abductive reasoning. J. Autom. Reason. 57(2), 97–134 (2016)MathSciNetCrossRef

Echenim, M., Peltier, N., Tourret, S.: An approach to abductive reasoning in equational logic. In: Proceedings of International Conference on Artificial Intelligence, IJCAI 2013, pp. 3–9. AAAI (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, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_10CrossRef

11.

Echenim, M., Peltier, N., Tourret, S.: Quantifier-free equational logic and prime implicate generation. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 311–325. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_21CrossRef

12.

Echenim, M., Peltier, N., Tourret, S.: Prime implicate generation in equational logic. J. Artif. Intell. Res. 60, 827–880 (2017)MathSciNetMATH

13.

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37CrossRef

14.

Fredkin, E.: Trie memory. Commun. ACM 3(9), 490–499 (1960)CrossRef

15.

Jackson, P.: Computing prime implicates incrementally. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 253–267. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_170CrossRef

16.

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

17.

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

18.

Marquis, P.: Extending abduction from propositional to first-order logic. In: Jorrand, P., Kelemen, J. (eds.) FAIR 1991. LNCS, vol. 535, pp. 141–155. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54507-7_12CrossRef

19.

Marquis, P.: Consequence finding algorithms. In: Kohlas, J., Moral, S. (eds.) Handbook of Defeasible Reasoning and Uncertainty Management Systems. HAND, vol. 5, pp. 41–145. Springer, Dordrecht (2000). https://doi.org/10.1007/978-94-017-1737-3_3CrossRef

20.

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). https://doi.org/10.1007/978-3-642-02716-1_19CrossRef

21.

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). https://doi.org/10.1007/978-3-642-21916-0_23CrossRef

22.

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

23.

Mishchenko, A.: An introduction to zero-suppressed binary decision diagrams. Technical report, Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (2001)

24.

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

25.

Previti, A., Ignatiev, A., Morgado, A., Marques-Silva, J.: Prime compilation of non-clausal formulae. In: Proceedings of the 24th International Conference on Artificial Intelligence, pp. 1980–1987. AAAI Press (2015)

26.

Quine, W.: A way to simplify truth functions. Am. Math. Mon. 62(9), 627–631 (1955)MathSciNetCrossRef

27.

Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 376–380. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45744-5_29CrossRefMATH

28.

Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_49CrossRef

29.

Simon, L., Del Val, A.: Efficient consequence finding. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence, pp. 359–370 (2001)

30.

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

31.

Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., Topić, D.: System description: Spass version 1.0.0. In: CADE 1999. LNCS, vol. 1632, pp. 378–382. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48660-7_34CrossRef

Title: A Generic Framework for Implicate Generation Modulo Theories
Authors: Mnacho Echenim
Nicolas Peltier
Yanis Sellami
Publisher: Springer International Publishing
Book: Automated Reasoning
Print ISBN: 978-3-319-94204-9

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

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-94205-6_19

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner