Free Variable Tableaux for a Logic with Term Declarations
- 222 Downloads
We study free variable tableau methods for logics with term declarations. We show how to define a substitutivity rule preserving the soundness of the tableaux and we prove that some other attempts lead to unsound systems. Based on this rule, we define a sound and complete free variable tableau system and we show how to restrict its application to close branches by defining a sorted unification calculus.
KeywordsFunction Symbol Predicate Symbol Constant Symbol Substitutivity Rule Tableau Method
Unable to display preview. Download preview PDF.
- [Coh 87]
- [Fit 96]M. Fitting. First-Order Logic and Automated Theorem Proving. Second edition. Springer, 1996.Google Scholar
- [Fri 91]
- [GLMN 96]A. Gavilanes, J. Leach, P. J. Martín, S. Nieva. Reasoning with preorders and dynamic sorts using free variable tableaux. Proc. AISMC-3. LNCS 1138, 365–379, 1996.Google Scholar
- [GLMN 97a]A. Gavilanes, J. Leach, P. J. Martín, S. Nieva. Ground semantic tableaux for a logic with preorders and dynamic declarations. TR DIA 50/97. 1997.Google Scholar
- [GLMN 97b]A. Gavilanes, J. Leach, P. J. Martín. Free variable tableaux for a logic with term declarations. TR DIA 69/97. 1997.Google Scholar
- [Kog 95]E. Kogel. Rigid E-unification simplified. Proc. 4th International Workshop TABLEAUX’95. LNCS 918, 17–30, 1995.Google Scholar
- [Sch 89]M. Schmidt-Schauss. Computational Aspects of an Order Sorted Logic with Term Declarations. LNAI 395. Springer, 1989.Google Scholar
- [Wal 87]C. Walther. A Many-sorted Calculus based on Resolution and Paramodulation. Research Notes in Artificial Intelligence. Pitman, 1987.Google Scholar
- [Wei 91]C. Weidenbach. A sorted logic using dynamic sorts. MPI-I-91-218, 1991.Google Scholar
- [Wei 95]