×

zbMATH — the first resource for mathematics

Inst-Gen – a modular approach to instantiation-based automated reasoning. (English) Zbl 1385.68038
Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 239-270 (2013).
Summary: Inst-Gen is an instantiation-based reasoning method for first-order logic introduced in [H. Ganzinger and the author, “New directions in instantiation-based theorem proving”, in: Proceedings of the 18th annual IEEE symposium on logic in computer science, LICS’03. Los Alamitos, CA: IEEE Computer Society. 55–64 (2003; doi:10.1109/LICS.2003.1210045)]. One of the distinctive features of Inst-Gen is a modular combination of first-order reasoning with efficient ground reasoning. Thus, Inst-Gen provides a framework for utilising efficient off-the-shelf propositional SAT and SMT solvers as part of general first-order reasoning. In this paper we present a unified view on the developments of the Inst-Gen method: (i) completeness proofs; (ii) abstract and concrete criteria for redundancy elimination, including dismatching constraints and global subsumption; (iii) implementation details and evaluation.
For the entire collection see [Zbl 1259.03008].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Akbarpour, B., Paulson, L.C.: Extending a Resolution Prover for Inequalities on Elementary Functions. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 47–61. Springer, Heidelberg (2007) · Zbl 1137.68571 · doi:10.1007/978-3-540-75560-9_6
[2] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University press, Cambridge (1998) · Zbl 0948.68098 · doi:10.1017/CBO9781139172752
[3] Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 2, pp. 19–99. Elsevier Science (2001) · Zbl 0993.03008 · doi:10.1016/B978-044450813-3/50004-7
[4] Baumgartner, P.: Logical Engineering with Instance-Based Methods. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 404–409. Springer, Heidelberg (2007) · Zbl 05523790 · doi:10.1007/978-3-540-73595-3_30
[5] Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Applied Logic 7(1), 58–74 (2009) · Zbl 1171.68040 · doi:10.1016/j.jal.2007.07.005
[6] Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. International Journal on Artificial Intelligence Tools 15(1), 21–52 (2006) · Zbl 05421296 · doi:10.1142/S0218213006002552
[7] Baumgartner, P., Schmidt, R.A.: Blocking and Other Enhancements for Bottom-Up Model Generation Methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 125–139. Springer, Heidelberg (2006) · Zbl 1222.68357 · doi:10.1007/11814771_11
[8] Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 350–364. Springer, Heidelberg (2003) · Zbl 1278.68249 · doi:10.1007/978-3-540-45085-6_32
[9] Brand, D.: Proving theorems with the modification method. SIAM J. Comput. 4(4), 412–430 (1975) · Zbl 0333.68059 · doi:10.1137/0204036
[10] Caferra, R., Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation 13(6), 613–641 (1992) · Zbl 0770.68104 · doi:10.1016/S0747-7171(10)80014-8
[11] Claessen, K., Sorensson, N.: New techniques that improve mace-style finite model finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (MODEL 2003) (2003)
[12] de Moura, L., Bjørner, N.S.: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 410–425. Springer, Heidelberg (2008) · Zbl 1165.03320 · doi:10.1007/978-3-540-71070-7_35
[13] Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT - A distributed and learning equational prover. Journal of Automated Reasoning 18(2), 189–198 (1997) · Zbl 05468571 · doi:10.1023/A:1005879229581
[14] Eén, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005) · Zbl 1128.68463 · doi:10.1007/11499107_5
[15] 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) · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37
[16] Eiter, T., Faber, W., Traxler, P.: Testing Strong Equivalence of Datalog Programs - Implementation and Examples. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 437–441. Springer, Heidelberg (2005) · Zbl 1152.68404 · doi:10.1007/11546207_42
[17] Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: Bloem, R., Sharygina, N. (eds.) The 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010), pp. 137–144. IEEE (2010)
[18] Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposium on LICS, pp. 55–64. IEEE (2003) · doi:10.1109/LICS.2003.1210045
[19] Ganzinger, H., Korovin, K.: Integrating Equational Reasoning into Instantiation-Based Theorem Proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 71–84. Springer, Heidelberg (2004) · Zbl 1095.68111 · doi:10.1007/978-3-540-30124-0_9
[20] Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 497–511. Springer, Heidelberg (2006) · Zbl 1165.03315 · doi:10.1007/11916277_34
[21] Graf, P.: Term Indexing. LNCS, vol. 1053. Springer, Heidelberg (1996) · Zbl 0970.68152
[22] Heule, M., Järvisalo, M., Biere, A.: Clause Elimination Procedures for CNF Formulas. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 357–371. Springer, Heidelberg (2010) · Zbl 1306.68144 · doi:10.1007/978-3-642-16242-8_26
[23] Hoder, K., Kovács, L., Voronkov, A.: Interpolation and Symbol Elimination in Vampire. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 188–195. Springer, Heidelberg (2010) · Zbl 1291.68348 · doi:10.1007/978-3-642-14203-1_16
[24] Hooker, J.N., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first order logic. Journal of Automated Reasoning 28, 371–396 (2002) · Zbl 0995.03010 · doi:10.1023/A:1015854101244
[25] Hustadt, U., Motik, B., Sattler, U.: Reducing SHIQ-description logic to disjunctive datalog programs. In: The Ninth International Conference on Principles of Knowledge Representation and Reasoning, pp. 152–162. AAAI Press (2004)
[26] Hustadt, U., Schmidt, R.: MSPASS: Modal Reasoning by Translation and First-Order Resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 67–71. Springer, Heidelberg (2000) · Zbl 0963.68522 · doi:10.1007/10722086_7
[27] Kapur, D., Narendran, P., Rosenkrantz, D., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991) · Zbl 0721.68032 · doi:10.1007/BF01893885
[28] Khasidashvili, Z., Kinanah, M., Voronkov, A.: Verifying equivalence of memories using a first order logic theorem prover. In: The 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), pp. 128–135. IEEE (2009) · doi:10.1109/FMCAD.2009.5351132
[29] Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Francaise d’Intelligence Artificielle 4(3), 9–52 (1990); Special issue on automated deduction
[30] Korovin, K.: iProver v0.2. In: Sutcliffe, G. (ed.) The CADE-21 ATP System Competition (CASC-21) (2007), see also [31]
[31] Korovin, K.: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008) · Zbl 1165.68462 · doi:10.1007/978-3-540-71070-7_24
[32] Korovin, K., Sticksel, C.: iProver-Eq: An Instantiation-Based Theorem Prover with Equality. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 196–202. Springer, Heidelberg (2010) · Zbl 1291.68354 · doi:10.1007/978-3-642-14203-1_17
[33] Korovin, K., Sticksel, C.: Labelled Unit Superposition Calculi for Instantiation-Based Reasoning. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 459–473. Springer, Heidelberg (2010) · Zbl 1306.68192 · doi:10.1007/978-3-642-16242-8_33
[34] Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. Journal of Automated Reasoning 3(3), 301–317 (1987) · Zbl 0641.68124 · doi:10.1007/BF00243794
[35] Lee, S.-J., Plaisted, D.: Eliminating duplication with the Hyper-linking strategy. Journal of Automated Reasoning 9, 25–42 (1992) · Zbl 0784.68077 · doi:10.1007/BF00247825
[36] Lynch, C., McGregor, R.E.: Combining Instance Generation and Resolution. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 304–318. Springer, Heidelberg (2009) · Zbl 1193.03028 · doi:10.1007/978-3-642-04222-5_19
[37] McCune, W.: OTTER 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory (1994)
[38] Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 371–443. Elsevier (2001) · Zbl 0997.03012 · doi:10.1016/B978-044450813-3/50009-6
[39] Navarro Pérez, J.A.: Encoding and Solving Problems in Effectively Propositional Logic. PhD thesis, University of Manchester (2007)
[40] Navarro-Pérez, J.A., Voronkov, A.: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 346–361. Springer, Heidelberg (2007) · Zbl 1213.68386 · doi:10.1007/978-3-540-73595-3_24
[41] Navarro, J.A., Voronkov, A.: Proof Systems for Effectively Propositional Logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 426–440. Springer, Heidelberg (2008) · Zbl 1165.03318 · doi:10.1007/978-3-540-71070-7_36
[42] Pichler, R.: Explicit versus implicit representations of subsets of the Herbrand universe. Theor. Comput. Sci. 290(1), 1021–1056 (2003) · Zbl 1051.68061 · doi:10.1016/S0304-3975(02)00583-2
[43] Plaisted, D., Zhu, Y.: Ordered semantic hyper-linking. J. Autom. Reasoning 25(3), 167–217 (2000) · Zbl 0959.68115 · doi:10.1023/A:1006376231563
[44] Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1853–1964. Elsevier and MIT Press (2001) · Zbl 0992.68189
[45] Riazanov, A., Voronkov, A.: Splitting without backtracking. In: Proc. of the 17 International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 611–617. Morgan Kaufmann (2001)
[46] Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(2-3), 91–110 (2002) · Zbl 1021.68082
[47] Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2-3), 111–126 (2002) · Zbl 1020.68084
[48] Schulz, S.: Simple and Efficient Clause Subsumption with Feature Vector Indexing. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proc. of the IJCAR-2004 Workshop on Empirically Successful First-Order Theorem Proving, Cork, Ireland. ENTCS. Elsevier Science (2004) · Zbl 1383.68082
[49] Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 441–456. Springer, Heidelberg (2010) · Zbl 1291.68372 · doi:10.1007/978-3-642-14203-1_38
[50] Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), 337–362 (2009) · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8
[51] Sutcliffe, G.: CASC-23 proceedings of the CADE-23 ATP system competition (2011), http://www.cs.miami.edu/ tptp/CASC/23/Proceedings.pdf
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.