Abstract
Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. The knowledge from a given domain (or theory) is made use of by applying efficient methods for reasoning in that domain. The general purpose foreground reasoner calls a special purpose background reasoner to handle problems from a certain theory.
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
P. B. Andrews. Theorem proving through general matings. Journal of the ACM, 28: 193–214, 1981.
L. Bachmair, H. Ganzinger and A. Voronkov. Elimination of equality via transformation with ordering constraints. Technical Report MPI–I–97–2–012, MPI für Informatik, Saarbrücken, 1997.
P. Baumgartner. A model elimination calculus with built-in theories. In H.-J. Ohlbach, editor, Proceedings, German Workshop on Artificial Intelligence (GWAI), LNCS 671, pages 30–42. Springer, 1992.
P. Baumgartner. Linear and unit-resulting refutations fer Horn theories. Journal of Automated Reasoning, 16 (3): 241–319, 1996.
P. Baumgartner. Theory Reasoning in Connection Calculi. LNCS. Springer, 1998. To appear.
P. Baumgartner, U. Furbach, and U. Petermann. A unified approach to theory reasoning. Forschungsbericht 15/92, University of Koblenz, 1992.
P. Baumgartner and U. Petermann. Theory reasoning. In W. Bibel and P. H. Schmitt, editors, Automated Deduction — A Basis for Applications, volume I. Kluwer, 1998.
G. Becher and U. Petermann. Rigid unification by completion and rigid paramodulation. In B. Nebel and L. Dreschler-Fischer, editors, Proceedings, 18th German Annual Conference on Artificial Intelligence (KI-94), Saarbrücken, Germany, LNCS 861, pages 319–330. Springer, 1994.
B. Beckert. A completion-based method for mixed universal and rigid E-unification. In A. Bundy, editor, Proceedings, 12th International Conference on Automated Deduction (CADE), Nancy, France, LNCS 814, pages 678–692. Springer, 1994.
B. Beckert. Semantic tableaux with equality. Journal of Logic and Computation, 7 (1): 39–58, 1997.
B Beckert. Rigid E-unification. In W. Bibel and P. H. Schmitt, editors, Automated Deduction —A Basis for Applications, volume I. Kluwer, 1998.
B. Beckert and R. Hähnle. An improved method for adding equality to free variable semantic tableaux. In D. Kapur, editor, Proceedings, 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY, USA, LNCS 607, pages 507–521. Springer, 1992.
B. Beckert and R. Hähnle. Analytic tableaux. In W. Bibel and P. H. Schmitt, editors, Automated Deduction — A Basis for Applications, volume I. Kluwer, 1998.
B. Becken, R. Hähnle, P. Oel and M. Sulzmann. The tableau-based theorem prover 3IxlP, version 4.0. In Proceedings, 13th International Conference on Automated Deduction (CADE), New Brunswick, NJ, USA, LNCS 1104, pages 303–307. Springer, 1996.
B. Beckett and C. Pape. Incremental theory reasoning methods for semantic tableaux. In P. Miglioli, U. Moscato, D. Mundici, and M. Omaghi, editors, Proceedings, 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Palermo, Italy, LNCS 1071, pages 93–109. Springer, 1996.
W. Bibel. Automated Theorem Proving. Vieweg, Braunschweig, second edition, 1987. First edition published in 1982.
D. Brand. Proving theorems with the modification method. SIAM Journal on Computing, 4 (4): 412–430, 1975.
R. J. Browne. Ground term rewriting in semantic tableaux systems for first-order logic with equality. Technical Report UMIACS-TR-88–44, College Park, MD, 1988.
H. Bürckert. A resolution principle for clauses with constraints. In Proceedings, 10th International Conference on Automated Deduction (CADE), LNCS 449, pages 178–192. Springer, 1990.
D. Cantone, A. Ferro and E. Omodeo. Computable Set Theory, volume 6 of International Series of Motwgraphs on Computer Science. Oxford University Press, 1989.
E. de Kogel. Rigid E-unification simplified. In Proceedings, 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, St. Goar, LNCS 918, pages 17–30. Springer, 1995.
A. Degtyarev and A. Voronkov. Equality elimination for the tableau method. In J. Calmet and C. Limongelli, editors, Proceedings, International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO), Karlsruhe, Germany, LNCS 1128, pages 46–60, 1996.
A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. In H. Kleine Büning, editor, Proceedings, Annual Conference of the European Association for Computer Science Logic (CSL’95), LNCS 1092, pages 178–190. Springer, 1996.
A. Degtyarev and A. Voronkov. What you always wanted to know about rigid E-unification. Journal of Automated Reasoning, 20 (1): 47–80, 1998.
V. J. Digricoli and M. C. Harrison. Equality-based binary resolution. Journal of the ACM, 33 (2): 253–289, April 1986.
M. C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996. First edition, 1990.
U. Furbach. Theory reasoning in first order calculi. In K. v. Luck and H. Marburger, editors, Proceedings, Third Workshop on Information Systems and Artificial Intelligence, Hamburg, Germany, LNCS 777, pages 139–156. Springer, 1994.
J. H. Gallier, P. Narendran, D. Plaisted and W Snyder. Rigid E-unification is NP-complete. In Procceedings, Symposium on Logic in Computer Science (LICS) IEEE Press, 1988.
J. H. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-completeness and application to equational matings. Information and Computation, pages 129–195, 1990.
J. H. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. Journal of the ACM, 39 (2): 377–429, April 1992.
J. H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification, equational matings. In Proceedings, Symposium on Logic in Computer Science (LICS), Ithaka, NY, USA IEEE Press, 1987.
J. H. Gallier and W. Snyder. Designing unification procedures using transformations: A survey. Bulletin of the EATCS, 40: 273–326, 1990.
G. Grieser. An implementation of rigid E-unification using completion and rigid paramodulation. Forschungsbericht FITL-96–4, FIT Leipzig e.V., 1996.
Y. Gurevich and M. Veanes. Some undecidable problems related to the Herbrand theorem. UPMAIL Technical Report 138, Uppsala University, 1997.
R. C. Jeffrey. Formal Logic. Its Scope and Limits. McGraw-Hill, New York, 1967.
J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J. Lassez and G. Plotkin, editors, Computational Logic — Essays in Honor of Alan Robinson, pages 257–321. MIT Press, 1991.
S. Kanger. A simplified proof method for elementary logic. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems,pages 87–94. North Holland, 1963. Reprint as pages 364–371, Siekmann, J., and Wrightson, G. (eds.), Automation of Reasoning. Classical Papers on Computational Logic,vol. 1. Springer, 1983.
D. Kozen. Positive first-order logic is NP-complete. IBM Journal of Research and Development, 25 (4): 327–332, 1981.
Z. Lis. Wynikanie semantyczne a wynikanie formalise. Studia Logica,10:39–60, 1960. In Polish with English summary.
D. W. Loveland. A simplified format for the model elimination procedure. Journal of the ACM, 16 (3): 233–248, 1969.
N. V. Murray and E. Rosenthal. Inference with path resolution and semantic graphs. Journal of the ACM, 34 (2): 225–254, April 1987.
N. V. Murray and E. Rosenthal. Theory links: Applications to automated theorem proving. Journal of Symbolic Computation, 4: 173–190, 1987.
G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27 (2): 356–364, April 1980.
R. Nieuwenhuis and A. Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computation, 19: 321–351, 1995.
U. Petermann. How to build-in an open theory into connection calculi. Journal on Computer and Artificial Intelligence, 11 (2): 105–142, 1992.
U. Petermann. Completeness of the pool calculus with an open built-in theory. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Proceedings, 3rd Kurt Gödel Colloquium (KGC), Brno, Czech Republic, LNCS 713, pages 264–277. Springer, 1993.
D. A. Plaisted. Special cases and substitutes for rigid E–unification. Technical Report MPI–I–95–2–010, Max–Planck–Institut für Informatik, Saarbrücken, November 1995.
A. Policriti and J. T. Schwartz. T-theorem proving I. Journal of Symbolic Computation, 20: 315–342, 1995.
R. J. Popplestone. Beth-tree methods in automatic theorem proving. In N. Collins and D. Michie, editors, Machine Intelligence, volume 1, pages 31–46. Oliver and Boyd, 1967.
S. V. Reeves. Adding equality to semantic tableau. Journal of Automated Reasoning, 3: 225–246, 1987.
J. A. Robinson and L. Wos. Paramodulation and theorem proving in first order theories with equality. In B. Meltzer and D. Michie, editors, Machine Intelligence. Edinburgh University Press, 1969.
R. E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21 (7): 583–585, 1978.
J. H. Siekmann. Universal unification. Journal of Symbolic Computation,7(3/4):207–274, 1989. Earlier version in Proceedings, 7th International Conference on Automated Deduction (CADE), Napa, FL. USA,LNCS 170, Springer, 1984.
R. M. Smullyan. First-Order Logic. Dover Publications, New York, second corrected edition, 1995. First published in 1968 by Springer.
W. Snyder. A Proof Theory for General Unification. Birkhäuser, Boston, 1991.
M. E. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, 1: 333–355, 1985.
M. Veanes. On Simultaneous Rigid E-Unification. PhD Thesis, Uppsala University, Sweden, 1997.
P. Voda and J. Komara. On Herbrand skeletons. Technical Report mff-ii-02–1995, Institute of Informatics, Comenius University, Bratislava, Slovakia, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Beckert, B. (1999). Equality and Other Theories. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds) Handbook of Tableau Methods. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-1754-0_4
Download citation
DOI: https://doi.org/10.1007/978-94-017-1754-0_4
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5184-4
Online ISBN: 978-94-017-1754-0
eBook Packages: Springer Book Archive