Abstract
Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a perfect term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the perfect model’s term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and complete for a first-order fixed domain semantics. For some classes of formulas and theories, we can even employ the calculus to prove properties of the perfect model itself, going beyond the scope of known superposition based approaches.
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
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4(3), 217–247 (1994)
Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol. 713, pp. 83–96. Springer, Heidelberg (1993)
Bouhoula, A.: Automated theorem proving by test set induction. J. Symb. Comp. 23(1), 47–77 (1997)
Caferra, R., Zabel, N.: A method for simultanous search for refutations and models by equational constraint solving. J. Symb. Comp. 13(6), 613–642 (1992)
Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation 7(3-4), 371–425 (1989)
Comon, H., Nieuwenhuis, R.: Induction = I-axiomatization + first-order consistency. Information and Computation 159(1/2), 151–186 (2000)
Ganzinger, H., Nivelle, H.D.: A superposition decision procedure for the guarded fragment with equality. In: Proc. of LICS 1999, pp. 295–305. IEEE, Los Alamitos (1999)
Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 226–241. Springer, Heidelberg (1993)
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)
Jacquemard, F., Rusinowitch, M., Vigneron, L.: Tree automata with equality constraints modulo equational theories. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 557–571. Springer, Heidelberg (2006)
Kapur, D., Narendran, P., Zhang, H.: Automating inductionless induction using test sets. Journal of Symbolic Computation 11(1/2), 81–111 (1991)
Nieuwenhuis, R.: Basic paramodulation and decidable theories (extended abstract). In: Proc. of LICS 1996, pp. 473–482. IEEE Computer Society Press, Los Alamitos (1996)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, ch. 7, vol. I, pp. 371–443. Elsevier, Amsterdam (2001)
Peltier, N.: Model building with ordered resolution: extracting models from saturated clause sets. Journal of Symbolic Computation 36(1-2), 5–48 (2003)
Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Handbook of Automated Reasoning, ch. 27, vol. 2, pp. 1965–2012. Elsevier, Amsterdam (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Horbach, M., Weidenbach, C. (2008). Superposition for Fixed Domains. In: Kaminski, M., Martini, S. (eds) Computer Science Logic. CSL 2008. Lecture Notes in Computer Science, vol 5213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87531-4_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-87531-4_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87530-7
Online ISBN: 978-3-540-87531-4
eBook Packages: Computer ScienceComputer Science (R0)