Free Variable Tableaux for a Logic with Term Declarations

  • P. J. Martín
  • A. Gavilanes
  • J. Leach
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


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.


Function Symbol Predicate Symbol Constant Symbol Substitutivity Rule Tableau Method 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Coh 87]
    A. G. Cohn. A more expressive formulation of many sorted logic. Journal of Automated Reasoning 3, 113–200, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  2. [Fit 96]
    M. Fitting. First-Order Logic and Automated Theorem Proving. Second edition. Springer, 1996.Google Scholar
  3. [Fri 91]
    A. M. Frisch. The substitutional framework for sorted deduction: fundamental results on hybrid reasoning. Artificial Intelligence 49, 161–198, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [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
  5. [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
  6. [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
  7. [Kog 95]
    E. Kogel. Rigid E-unification simplified. Proc. 4th International Workshop TABLEAUX’95. LNCS 918, 17–30, 1995.Google Scholar
  8. [Sch 89]
    M. Schmidt-Schauss. Computational Aspects of an Order Sorted Logic with Term Declarations. LNAI 395. Springer, 1989.Google Scholar
  9. [Wal 87]
    C. Walther. A Many-sorted Calculus based on Resolution and Paramodulation. Research Notes in Artificial Intelligence. Pitman, 1987.Google Scholar
  10. [Wei 91]
    C. Weidenbach. A sorted logic using dynamic sorts. MPI-I-91-218, 1991.Google Scholar
  11. [Wei 95]
    C. Weidenbach. First-order tableaux with sorts. J. of the Interest Group in Pure and Applied Logics 3(6), 887–907, 1995.zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • P. J. Martín
    • 1
  • A. Gavilanes
    • 1
  • J. Leach
    • 1
  1. 1.Dep. de Sistemas Informáticos y ProgramaciónUniversidad Complutense de MadridMadrid

Personalised recommendations