Abstract
A number of first-order calculi employ an explicit model representation formalism in support of non-redundant inferences and for detecting satisfiability. Many of these formalisms can represent infinite Herbrand models. The first-order fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism used in the approximation refinement calculus (AR). Our first result is a finite model property for MSLH clause sets. Therefore, MSLH clause sets cannot represent models of clause sets with inherently infinite models. Through a translation to tree automata, we further show that this limitation also applies to the linear fragments of implicit generalizations, which is the formalism used in the model-evolution calculus (ME), to atoms with disequality constraints, the formalisms used in the non-redundant clause learning calculus (NRCL), and to atoms with membership constraints, a formalism used for example in decision procedures for algebraic data types. Although these formalisms cannot represent models of clause sets with inherently infinite models, through an additional approximation step they can. This is our second main result. For clause sets including the definition of an equivalence relation with the help of an additional, novel approximation, called reflexive relation splitting, the approximation refinement calculus can automatically show satisfiability through the MSLH clause set formalism.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Alagi, G., Weidenbach, C.: NRCL – A model building approach to the Bernays-Schönfinkel fragment. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 69–84. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24246-0_5
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)
Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 572–586. Springer, Heidelberg (2006). https://doi.org/10.1007/11916277_39
Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: 2004 IEEE Symposium on Security and Privacy, pp. 86–100 (2004)
Bonacina, M.P., Furbach, U., Sofronie-Stokkermans, V.: On first-order model-based reasoning. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 181–204. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23165-5_8
Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reason. 56(2), 113–141 (2016). Inference System and Completeness in 59(2), JAR
Brainerd, W.S.: The minimalization of tree automata. Inf. Control 13, 484–491 (1968)
Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic Series, vol. 31. Kluwer, Dordrecht (2004). https://doi.org/10.1007/978-1-4020-2653-9
Claessen, K., Soerensson, N.: New techniques that improve mace-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)
Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007). http://tata.gforge.inria.fr/. Release 12 Oct 2007
Comon, H.: Disunification: A survey. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 322–359. The MIT Press, Cambridge (1991)
Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Springer, New York (1994). https://doi.org/10.1007/978-1-4757-2355-7
Fermüller, C.G., Pichler, R.: Model representation over finite and infinite signatures. J. Log. Comput. 17(3), 453–477 (2007)
Hernandez, J.C.L., Korovin, K.: Towards an abstraction-refinement framework for reasoning with large theories. In: IWIL@LPAR 2017. EasyChair (2017)
Jacquemard, F., Meyer, C., Weidenbach, C.: Unification in extensions of shallow equational theories. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 76–90. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0052362
Korovin, K.: Inst-Gen – A modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239–270. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37651-1_10
McCune, W.: Mace4 reference manual and guide. CoRR, cs.SC/0310055 (2003)
Peltier, N.: Constructing infinite models represented by tree automata. Ann. Math. Artif. Intell. 56, 65–85 (2009)
Piskac, R., de Moura, L.M., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reason. 44(4), 401–424 (2010)
Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. 52, 264–268 (1946)
Slaney, J.: FINDER: Finite domain enumerator system description. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 798–801. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58156-1_63
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)
Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17–23 January 2010, pp. 199–210. ACM (2010)
Teucke, A.: An approximation and refinement approach to first-order automated reasoning. Doctoral thesis, Saarland University (2018)
Teucke, A., Voigt, M., Weidenbach, C.: On the expressivity and applicability of model representation formalisms. arXiv preprint, arXiv:1905.03651 [cs.LO] (2019)
Teucke, A., Weidenbach, C.: First-order logic theorem proving and model building via approximation and instantiation. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 85–100. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24246-0_6
Teucke, A., Weidenbach, C.: Ordered resolution with straight dismatching constraints. In: Fontaine, P., Schulz, S., Urban, J. (eds.) 5th Workshop on Practical Aspects of Automated Reasoning (PAAR@IJCAR 2016) co-located with International Joint Conference on Automated Reasoning (IJCAR) 2016. CEUR Workshop Proceedings, vol. 1635, pp. 95–109. CEUR-WS.org (2016). http://ceur-ws.org/Vol-1635
Teucke, A., Weidenbach, C.: Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 202–219. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_13
Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48660-7_29
Weidenbach, C.: Automated reasoning building blocks. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 172–188. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23506-6_12
Acknowledgments
This work was funded by DFG grant 389792660 as part of TRR 248. We thank our reviewers for their valuable comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Teucke, A., Voigt, M., Weidenbach, C. (2019). On the Expressivity and Applicability of Model Representation Formalisms. In: Herzig, A., Popescu, A. (eds) Frontiers of Combining Systems. FroCoS 2019. Lecture Notes in Computer Science(), vol 11715. Springer, Cham. https://doi.org/10.1007/978-3-030-29007-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-29007-8_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29006-1
Online ISBN: 978-3-030-29007-8
eBook Packages: Computer ScienceComputer Science (R0)