Abstract
T-resolution is a binary rule, proposed by Policriti and Schwartz in 1995 for theorem proving in first-order theories (T-theorem proving) that can be seen – at least at the ground level – as a variant of Stickel's theory resolution. In this paper we consider refinements of this rule as well as the model elimination variant of it. After a general discussion concerning our viewpoint on theorem proving in first-order theories and a brief comparison with theory resolution, the power and generality of T-resolution are emphasized by introducing suitable linear and ordered refinements, uniformly and in strict analogy with the standard resolution approach. Then a model elimination variant of T-resolution is introduced and proved to be sound and complete; some experimental results are also reported. In the last part of the paper we present two applications of T-resolution: to constraint logic programming and to modal logic.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Baumgartner, P.: A model elimination calculus with built-in theories, in H. J. Ohlbach (ed.), Proceedings of the 16th German Conference on Artificial Intelligence, LNAI 671, Springer-Verlag, 1992.
Baumgartner, P.: An ordered theory resolution calculus, in Proceedings of the Conference on Logic Programming and Artificial Intelligence, LNAI 624, Springer-Verlag, 1992.
Baumgartner, P., Furbach, U. and Petermann, U.: A Unified Approach to Theory Reasoning, Technical Report 15/92, University of Koblenz, 1992.
van Benthem, J. F. A. K., D'Agostino, G., Montanari, A. and Policriti, A.: Modal deduction in second-order logic and set theory-I, J. Logic Comput. 7(2) (1996), 251-265.
van Benthem, J. F. A. K., D'Agostino, G., Montanari, A. and Policriti, A.: Modal deduction in second-order logic and set theory-II, Notre Dame J. Formal Logic, 1997, to appear.
van Benthem, J. F. A. K.: Modal Logic and Classical Logic, Bibliopolis, Napoli and Atlantic Heights, NJ, 1985.
Cantone, D., Ferro, A. and Omodeo, E. G.: Computable Set Theory, Vol. 1, International Series of Monographs on Computer Science, Clarendon Press, Oxford, 1989.
Carroll, L.: Lewis Carroll' Symbolic Logic, C. N. Potter, New York, 1977.
Chang, C. and Lee, R.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
Dovier, A., Formisano, A. and Policriti, A.: On T-logic programming, in J. Maluszynski (ed.), Proceedings of the International Logic Programming Symposium 1997. ILPS97, MIT Press.
D'Agostino, G., Montanari, A. and Policriti, A.: A set-theoretic translation method for polimodal logics, J. Automated Reasoning 15(3) (1995), 317-337.
Fleisig, S., Loveland, D., Smiley III, A. K. and Yarmush, D. L.: An implementation of the model elimination proof procedure, J. ACM 21(1) (1974).
Ferro, S. and Omodeo, E. G.: An efficient validity test for formulae in extensional two-level syllogistic, Le Matematiche 23(1) (1978), 130-137 (Catania, Italy).
Ferro, A., Omodeo, E. G. and Schwartz, J. T.: Decision procedures for elementary sublanguages of set theory I, Multilevel syllogistic and some extensions, Comm. Pure Appl. Math. 33 (1980), 599-608.
Hopcroft, J. E. and Ullman, J. D.: Introduction to Automata Theory, Languages and Computation, Addison-Wesley, Reading, MA, 1979.
Jaffar, J. and Lassez, J. L.: Constraint Logic Programming, Technical Report, Department of Computer Science, Monash University, June 1986.
Jaffar, J. and Maher, M. J.: Constraint logic programming: A survey, J. Logic Programming 19-20 (1994), 503-581.
Kowalsky, R. and Hayes, P. J.: Semantic Trees in Automatic Theorem-Proving, Machine Intelligence 4, Meltzer and Michie (eds.), Edinburgh University Press, 1969.
Loveland, D. W.: Automated Theorem Proving, North-Holland, Amsterdam, 1978.
Manthey, R. and Bry, F.: Satchmo: A theorem prover implemented in Prolog, Lecture Notes in Comput. Sci. 310 (1988), 415-434. CADE 9, 9th Conference on Automated Deduction.
Mendelson, E.: Introduction to Mathematical Logic, 2nd edn, D. Van Nostrand Company, New York, 1979.
Petermann, U.: Towards a connection procedure with built-in theories, in European Workshop on Logic in AI, LNAI 478, Springer-Verlag, 1990.
Petermann, U.: Completeness of the pool calculus with an open built-in theory, in G. Gottlob, A. Leitsch and A. Mundici (eds.), Computational Logic and Proof Theory. Proceedings of the 3rd K. G ö del Colloquium, LNCS 713, Springer-Verlag, 1993.
Policriti, A. and Schwartz, J. T.: T theorem proving I, J. Symbolic Comput. 20 (1995), 315-342.
Policriti, A. and Tetali, P.: On the Satisfiability Problem for the Ground Case of First Order Theories, Technical Report 38, DIMACS center, 1992.
Schwartz, J. T., Dewar, R. K. B., Dubinsky, E. and Schonberg, E.: Programming with Sets: An Introduction to SETL, Texts and Monographs in Computer Science, Springer-Verlag, 1986.
Stickel, M. E.: Theory resolution: Building in nonequational theories, in Proceedings of the AAAI-83, 1983, pp. 391-397.
Stickel, M. E.: Automated deduction by theory resolution, J. Automated Reasoning 1(4) (1985), 333-355.
Turchetti, D.: Sistemi di deduzione per logiche modali, Master' thesis, Università di Udine, Dip. di Matematica e Informatica, 1996. ?
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Formisano, A., Policriti, A. T-Resolution: Refinements and Model Elimination. Journal of Automated Reasoning 22, 433–483 (1999). https://doi.org/10.1023/A:1006170514174
Issue Date:
DOI: https://doi.org/10.1023/A:1006170514174