Abstract
Program semantics can often be expressed as a (many-sorted) first-order theory \(\mathcal{S}\), and program properties as sentences \(\varphi \) which are intended to hold in the canonical model of such a theory, which is often incomputable. Recently, we have shown that properties \(\varphi \) expressed as the existential closure of a boolean combination of atoms can be disproved by just finding a model of \(\mathcal{S}\) and the negation \(\lnot \varphi \) of \(\varphi \). Furthermore, this idea works quite well in practice due to the existence of powerful tools for the automatic generation of models for (many-sorted) first-order theories. In this paper we extend our previous results to arbitrary properties, expressed as sentences without any special restriction. Consequently, one can prove a program property \(\varphi \) by just finding a model of an appropriate theory (including \(\mathcal{S}\) and possibly something else) and an appropriate first-order formula related to \(\varphi \). Beyond its possible theoretical interest, we show that our results can also be of practical use in several respects.
Partially supported by the EU (FEDER), projects TIN2015-69175-C4-1-R, and GV PROMETEOII/2015/013.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A mapping \(f:A\rightarrow B\) is surjective if for all \(b\in B\) there is \(a\in A\) such that \(f(a)=b\).
- 2.
This proves \(\mathcal{R}\) ground locally confluent, i.e., variables in \(\varphi _{ WCR }\) refer to ground terms only; since \(\mathcal{R}\) is a ground TRS, local confluence and ground local confluence coincide.
- 3.
- 4.
- 5.
- 6.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)
Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002)
Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoret. Comput. Sci. 351(1), 386–414 (2006)
Clark, K.L.: Predicate logic as a computational formalism. Ph.D. thesis, Research Monograph 79/59 TOC, Department of Computing, Imperial College of Science, and Technology, University of London, December 1979
Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1
Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: Proceedings of LICS 1990, pp. 242–248. IEEE Press (1990)
Dershowitz, N., Kaplan, S., Plaisted, D.: Rewrite, rewrite, rewrite, rewrite, rewrite, \(\ldots \) Theoret. Comput. Sci. 83, 71–96 (1991)
Endrullis, J., Hendriks, D.: Lazy productivity via termination. Theoret. Comput. Sci. 412, 3203–3225 (2011)
Goguen, J.A., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol. 250, pp. 1–22. Springer, Heidelberg (1987). https://doi.org/10.1007/BFb0014969
Gutiérrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories. In: Proceedings of PROLE 2016, pp. 215–230 (2016). Tool available at http://zenon.dsic.upv.es/ages/
Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)
Kim, S., Zhang, H.: ModGen: theorem proving by model generation. In: Proceedings of AAAI 1994, pp. 162–167. AAAI Press/MIT Press (1994)
Kleene, S.C.: Mathematical Logic. Wiley, Hoboken (1967). (Dover 2002)
Lucas, S.: Analysis of rewriting-based systems as first-order theories. In: Fioravanti, F., Gallagher, J.P. (eds.) LOPSTR 2017. LNCS, vol. 10855, pp. 180–197. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94460-9_11
Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465–501 (2018)
Lucas, S., Gutiérrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90–95 (2018)
McCune, W.: Prover9 and Mace4 (2005–2010). http://www.cs.unm.edu/~mccune/prover9/
Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81, 721–781 (2012)
Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002). https://doi.org/10.1007/978-1-4757-3661-8
Reiter, R.: On closed world data bases. In: Logic and Data Bases, pp. 119–140. Plenum Press, New York (1978)
Reger, G., Suda, M., Voronkov, A.: Finding finite models in multi-sorted first-order logic. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 323–341. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_20
Shapiro, S.: Foundations Without Foundationalism: A Case for Second-Order Logic. Clarendon Press, Oxford (1991)
Wang, H.: Logic of many-sorted theories. J. Symbolic Logic 17(2), 105–116 (1952)
Zhang, J., Zhang, H.: Generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 308–312. Springer, New York (1996)
Acknowledgements
I thank the anonymous referees for their comments and suggestions. I also thank Philipp Rümmer and Mohamed Iguernlala for their clarifying remarks about the use of Princess and Alt-Ergo, respectively.
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
Lucas, S. (2019). Proving Program Properties as First-Order Satisfiability. In: Mesnard, F., Stuckey, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2018. Lecture Notes in Computer Science(), vol 11408. Springer, Cham. https://doi.org/10.1007/978-3-030-13838-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-13838-7_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-13837-0
Online ISBN: 978-3-030-13838-7
eBook Packages: Computer ScienceComputer Science (R0)