zbMATH — the first resource for mathematics

Nanocop: a non-clausal connection prover. (English) Zbl 06623269
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 302-312 (2016).
Summary: Most of the popular efficient proof search calculi work on formulae that are in clausal form, i.e. in disjunctive or conjunctive normal form. Hence, most state-of-the-art fully automated theorem provers require a translation of the input formula into clausal form in a preprocessing step. Translating a proof in clausal form back into a more readable non-clausal proof of the original formula is not straightforward. This paper presents a non-clausal theorem prover for classical first-order logic. It is based on a non-clausal connection calculus and implemented with a few lines of Prolog code. By working entirely on the original structure of the input formula, the resulting non-clausal proofs are not only shorter, but can also be more easily translated into, e.g., sequent proofs. Furthermore, a non-clausal proof search is more suitable for some non-classical logics.
For the entire collection see [Zbl 1337.68016].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Andrews, P.B.: Theorem proving via general matings. J. ACM 28, 193–214 (1981) · Zbl 0456.68119
[2] Antonsen, R., Waaler, A.: Liberalized variable splitting. J. Autom. Reasoning 38, 3–30 (2007) · Zbl 1121.03019
[3] Beckert, B., Posegga, J.: leanTAP: lean, tableau-based deduction. J. Autom. Reasoning 15(3), 339–358 (1995) · Zbl 0838.68097
[4] Bibel, W.: Matings in matrices. Communications of the ACM, pp. 844–852 (1983) · Zbl 0519.68078
[5] Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg, Wiesbaden (1987) · Zbl 0639.68092
[6] Gentzen, G.: Untersuchungen über das logische Schließen. Math. Z. 39, 176–210 (1935) · JFM 60.0020.02
[7] Hähnle, R.: Tableaux and related methods. In: Handbook of Automated Reasoning, pp. 100–178. Elsevier, Amsterdam (2001) · Zbl 1011.68125
[8] Hähnle, R., Murray, N., Rosenthal, E.: Linearity and regularity with negation normal form. Theoret. Comput. Sci. 328, 325–354 (2004) · Zbl 1071.68091
[9] Issar, S.: Path-focused duplication: a search procedure for general matings. In: AAAI 1990 Proceedings, pp. 221–226 (1990)
[10] Kaliszyk, C., Urban, J.: FEMaLeCoP: fairly efficient machine learning connection prover. In: Davis, M., et al. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 88–96. Springer, Heidelberg (2015) · Zbl 06528775
[11] Kreitz, C., Otten, J.: Connection-based theorem proving in classical and non-classical logics. J. Univ. Comput. Sci. 5, 88–112 (1999) · Zbl 0961.68118
[12] McCune, W.: Release of prover9. Mile high conference on quasigroups, loops and nonassociative systems (2005)
[13] Otten, J.: \[ {\mathsf leanCoP 2.0} \] and \[ {\mathsf ileanCoP 1.2} \] : high performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 283–291. Springer, Heidelberg (2008) · Zbl 1165.68467
[14] Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23, 159–182 (2010) · Zbl 1205.68363
[15] Otten, J.: A non-clausal connection calculus. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 226–241. Springer, Heidelberg (2011) · Zbl 1333.03004
[16] Otten, J.: \[ \mathsf MleanCoP \] : a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 269–276. Springer, Heidelberg (2014) · Zbl 1423.68423
[17] Otten, J., Bibel, W.: Advances in connection-based automated theorem proving. In: Bowen, J., Hinchey, M., Olderog, E.-R. (eds.) Provably Correct Systems (to appear) · Zbl 1025.68076
[18] Otten, J., Bibel, W.: \[ {\mathsf leanCoP} \] : lean connection-based theorem proving. J. Symbolic Comput. 36, 139–161 (2003) · Zbl 1025.68076
[19] Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symbolic Comput. 2, 293–304 (1986) · Zbl 0636.68119
[20] Reis, G.: Importing SMT and connection proofs as expansion trees. In: Kaliszyk, C., Paskevich, A. (eds.) 4th Workshop on Proof eXchange for Theorem Proving (PxTP15), EPTCS 186, pp. 3–10 (2015)
[21] Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: \[ JProver \] : integrating connection-based theorem proving into interactive proof assistants. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 421–426. Springer, Heidelberg (2001) · Zbl 0988.68609
[22] Schulz, S.: E - a Brainiac theorem prover. AI Commun. 15(2), 111–126 (2002) · Zbl 1020.68084
[23] Stickel, M.: A prolog technology theorem prover: implementation by an extended prolog compiler. J. Autom. Reasoning 4, 353–380 (1988) · Zbl 0662.68104
[24] Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337–362 (2009) · Zbl 1185.68636
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.