Abstract
The concept of redundancy and simplification has been an ongoing theme in Harald Ganzinger’s work from his first contributions to equational completion to the various variants of the superposition calculus. When executed by a theorem prover, the inference rules of logic calculi usually generate a tremendously huge search space. The redundancy and simplification concept is indispensable for cutting down this search space to a manageable size. For a number of subclasses of first-order logic appropriate redundancy and simplification concepts even turn the superposition calculus into a decision procedure. Hence, the key to successfully applying first-order theorem proving to a problem domain is to find those simplifications and redundancy criteria that fit this domain and can be effectively implemented.
We present Harald Ganzinger’s work in the light of the simplification and redundancy techniques that have been developed for concrete problem areas. This includes a variant of contextual rewriting to decide a subclass of Euclidean geometry, ordered chaining techniques for Church-Rosser and priority queue proofs, contextual rewriting and history- dependent complexities for the completion of conditional rewrite systems, rewriting with equivalences for theorem proving in set theory, soft typing for the exploration of sort information in the context of equations, and constraint inheritance for automated complexity analysis.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Afshordel, B., Hillenbrand, T., Weidenbach, C.: First-Order Atom Definitions Extended. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 309–319. Springer, Heidelberg (2001)
Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, New York (1998)
Bachmair, L.: Canonical Equational Proofs. Birkhäuser, Boston (1991)
Bachmair, L., Dershowitz, N., Hsiang, J.: Orderings for equational proofs. In: [First Annual] Symposium on Logic in Computer Science, June 16–18, pp. 346–357. IEEE Computer Society Press, Cambridge (1986)
Bachmair, L., Ganzinger, H.: Completion of First-Order Clauses with Equality by Strict Superposition (extended abstract). In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol. 516, pp. 162–180. Springer, Heidelberg (1991)
Bachmair, L., Ganzinger, H.: On Restrictions of Ordered Paramodulation with Simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 427–441. Springer, Heidelberg (1990)
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.: Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM 45(6), 1007–1049 (1998)
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, ch. 2, pp. 19–99. Elsevier (2001)
Balbiani, P.: Equation Solving in Geometrical Theories. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol. 968, Springer, Heidelberg (1995)
Balbiani, P.: Mécanisation de la géométrie: incidence et orthogonalité. Revue d’Intelligence Artificielle 11, 179–211 (1997)
Basin, D., Ganzinger, H.: Automated complexity analysis based on ordered resolution. Journal of the ACM 48(1), 70–109 (2001)
Bertling, H., Ganzinger, H., Schäfers, R.: CEC: A System for the Completion of Conditional Equational Specifications. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 378–379. Springer, Heidelberg (1988)
Brinker, C.: Geometrisches Schließen mit SPASS. Diplomarbeit, Universität des Saarlandes and Max-Planck-Institut für Informatik, Saarbrücken, Germany (2000); Supervisors: Ganzinger, H., Weidenbach, C.
de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church–Rosser theorem. Indagationes Mathematicae 34(5), 381–392 (1972)
Church, A.: An unsolvable problem of elementary number theory. American Journal of Mathematics 58, 345–363 (1936)
Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. Journal of the ACM 27(4), 758–771 (1980)
Fay, M.: First-order unification in an equational theory. In: Fourth Workshop on Automated Deduction, pp. 161–167. Academic Press, Austin (1979)
Finkler, U., Mehlhorn, K.: Checking priority queues. In: Proceedings of the 10th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 1999). Society for Industrial and Applied Mathematics, pp. 901–902 (1999)
Ganzinger, H.: A Completion Procedure for Conditional Equations. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 62–83. Springer, Heidelberg (1988)
Ganzinger, H.: Completion with History-Dependent Complexities for Generated Equations. In: Sannella, D., Tarlecki, A. (eds.) Abstract Data Types 1987. LNCS, vol. 332, pp. 73–91. Springer, Heidelberg (1988)
Ganzinger, H.: Ground Term Confluence in Parametric Conditional Equational Specifications. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol. 247, pp. 286–298. Springer, Heidelberg (1987)
Ganzinger, H.: A completion procedure for conditional equations. Journal of Symbolic Computation 11, 51–81 (1991)
Ganzinger, H.: Order-sorted completion: the many-sorted way. Theoretical Computer Science 89, 3–32 (1991)
Ganzinger, H., Meyer, C., Weidenbach, C.: Soft Typing for Ordered Resolution. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 321–335. Springer, Heidelberg (1997)
Ganzinger, H., Nieuwenhuis, R., Nivela, P.: The Saturate system (1994), http://www.mpi-sb.mpg.de/SATURATE
Ganzinger, H., Schäfers, R.: System support for modular order-sorted horn clause specifications. In: 12th International Conference on Software Engineering, pp. 150–159. IEEE Computer Society Press, Nice (1990)
Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Information and Computation 199, 3–23 (2005)
Giegerich, R.: Specification and correctness of code generators – an experiment with the CEC-system. In: Müller, J., Ganzinger, H. (eds.) 1st German Workshop “Term Rewriting: Theory and Applications”, SEKI-Report 89/02. Universität Kaiserslautern (1989)
Gnaedig, I., Kirchner, C., Kirchner, H.: Equational completion in order-sorted algebras. Theoretical Computer Science 72(2&3), 169–202 (1990)
Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem-proving strategies: The transfinite semantic tree method. Journal of the ACM 38(3), 559–587 (1991)
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)
Kleene, S.: A theory of positive integers in formal logic. American Journal of Mathematics 57, 153–173, 219–244 (1935)
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970); Reprinted in Siekmann and Wrightson [50], pp. 342–376
McAllester, D.A.: Automatic recognition of tractability in inference relation. Journal of the ACM 40(2), 284–303 (1993)
Nieuwenhuis, R.: First-order completion techniques. Technical report, UPC-LSI, Cited in Nieuwenhuis and Rubio [38] (1991)
Nieuwenhuis, R.: Basic paramodulation and decidable theories (extended abstract). In: Proceedings 11th IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 473–482. IEEE Computer Society Press (1996)
Nieuwenhuis, R., Rubio, A.: Basic Superposition is Complete. In: Krieg-Brückner, B. (ed.) ESOP 1992. LNCS, vol. 582, Springer, Heidelberg (1992)
Nipkow, T.: More Church–Rosser proofs (in Isabelle/HOL). Journal of Automated Reasoning 26, 51–66 (2001)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Nivela, P., Nieuwenhuis, R.: Saturation of First-Order (constrained) Clauses with the Saturate System. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 436–440. Springer, Heidelberg (1993)
de Nivelle, H., Piskac, R.: Verification of an off-line checker for priority queues. In: Aichernig, B.K., Beckert, B. (eds.) Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), pp. 210–219. IEEE, Koblenz (2005)
Ohlbach, H.J.: Translation methods for non-classical logics – an overview. Bulletin of the IGPL 1(1), 69–90 (1993)
Peterson, G.E.: A technique for establishing completeness results in theorem proving with equality. SIAM Journal on Computing 12(1), 82–100 (1983)
Piskac, R.: Formal correctness of result checking for priority queues. Master’s thesis, Universität des Saarlandes (February 2005)
Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Communications 15(2-3), 91–110 (2002)
Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, ch. 8, pp. 298–313. Edinburgh University Press, Edinburgh (1969); Reprinted in Siekmann and Wrightson [50], pp. 298–313
Rusinowitch, M.: Theorem-proving with resolution and superposition. Journal of Symbolic Computation 11(1&2), 21–49 (January/February 1991)
Schulz, S.: E – A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002)
Siekmann, J., Wrightson, G.: Automation of Reasoning: Classical Papers on Computational Logic 1967-1970, vol. 2. Springer, Berlin (1983)
Takahashi, M.: Parallel reductions in λ-calculus. Information and Computation 118(1), 120–127 (1995)
Wasserman, H., Blum, M.: Software reliability via run-time result-checking. Journal of the ACM 44(6), 826–849 (1997)
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., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS Version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 275–277. Springer, Heidelberg (2002)
Weidenbach, C., Gaede, B., Rock, G.: SPASS & FLOTTER, version 0.42. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol. 1104, pp. 141–145. Springer, Heidelberg (1996)
Zhang, H., Kapur, D.: First-Order Theorem Proving using Conditional Rewrite Rules. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 1–20. Springer, Heidelberg (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hillenbrand, T., Piskac, R., Waldmann, U., Weidenbach, C. (2013). From Search to Computation: Redundancy Criteria and Simplification at Work. In: Voronkov, A., Weidenbach, C. (eds) Programming Logics. Lecture Notes in Computer Science, vol 7797. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37651-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-37651-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37650-4
Online ISBN: 978-3-642-37651-1
eBook Packages: Computer ScienceComputer Science (R0)