### Theorem proving with built-in hybrid theories

DOI: http://dx.doi.org/10.12775/LLP.1998.005

#### Abstract

#### Full Text:

PDF#### References

Baumgartner, P., “Theory Model Elimination”, in H. J. Ohlbach (ed.), Proc. GWAI 92, 1992, MP-I-Inf.

Baumgartner, P., Theory Reasoning in Connection Calculi and the Linearizing Completion Approach, PhD thesis, Universität Koblenz-Landau, 1996.

Baumgartner, P., and F. Stolzenburg, “Constraint model elimination and a pttp-implementation”, in Proceedings Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, 201–216, Springer, 1995.

Bibel, W., Automated Theorem Proving, Vieweg Verlag, Braunschweig, 1982.

Boyreau, Un atelier de demonstration automatique multilogique. Application a la logique modale et l’unification associativee. PhD thesis, Université de Caen, 1994.

Bürckert, H.-J., “A resolution principle for constrained logics”, Artificial Intelligence 66:235–271, 1994.

Clerin-Debart, F., Th´eories ´equationelles et de contraintes pour la d´emonstration automatique en logique multi-modale, PhD thesis, Laboratoire d’Informatique, Université de Caen, France, Jan. 1992.

Debart, F., and P. Enjalbert, “A case of termination for associative unification”, in J. P. H. Abdulrab (ed.), Words Equtions and related Topics: Second International Workshop IWWERT ’91, Berlin, 1992, Springer-Verlag.

Debart, F., P. Enjalbert, and M. Lescot. “Multi Modal Logic Programming Using Equational and Order-Sorted Logic”, in M. Okada and S. Kaplan, editors, Proc. 2nd Conf. on Conditional and Typed Rewriting Systems, Springer, 1990, LNCS.

Frisch, A. M., ‘The Substitutional Framework for Sorted Deduction: Fundamental Results on Hybrid Reasoning”, Artificial Intelligence, 1991.

Frisch, A. M., and R. B. Scherl, “A General Framework for Modal Deduction”, in Principles of Knowledge Representation and Reasoning, Proceedings of KR’91, 1991.

Genesereth, M., and N. Nilsson, Logical Foundations of Artificial Intelligence, Morgan Kauffman, Los Altos, California, 1987.

Kripke, S., “Semantical analysis of modal logic I. Normal propositional calculi”, Zeitschrift f¨ur mathematische Logik und Grundlagen der Mathematik 9:67–96, 1963.

Loveland, D., Automated Theorem Proving – A Logical Basis, North Holland, 1978.

Miller, D. A., Proofs in Higher-Order Logic, PhD thesis, Carnegie Mellon University, Pittsburg Pa., 1983.

Neugebauer, G., and U. Petermann, “Specifications of inference rules and their automatic translation”, in Proceedings Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, p. 185–200, Springer, 1995.

Neugebauer, G., and T. Schaub, “A pool-based connection calculus”, in C. Bozsahin, U. Halıcı, K. Oflazar, and N. Yalabık (eds.), Proceedings of Third Turkish Symposium on Artificial Intelligence and Neural Networks, p. 297–306, Middle East Technical University Press, 1994.

Ohlbach, H. J., and R. Schmidt, “Functional translation and second-order frame properties of modal logic”, Research Report MPI-I-95-2-002, Max-Planck-Institut für Informatik, Im Stadtwald D 66123 Saarbrücken, jan 1995.

Petermann, U., “How to Build-in an Open Theory into Connection Calculi”, Journal on Computer and Artificial Intelligence 11(2):105–142, 1992.

Petermann, U., “Completeness of the pool calculus with an open built in theory”, in G. Gottlob, A. Leitsch, and D. Mundici (eds.), 3rd Kurt Gödel Colloquium ’93, volume 713 of Lecture Notes in Computer Science, Springer-Verlag, 1993.

Rigó, Z., “Untersuchungen zum automatischen Beweisen in Modallogiken”, Master’s thesis, Universität Leipzig, 1995.

Stickel, M., “Automated deduction by theory resolution”, J. of Automated Reasoning, 4(1):333–356, 1985.

ISSN: 2300-9802 (electronic version)