Reasoning with preorders and dynamic sorts using free variable tableaux

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


In this paper we present a three valued many sorted logic for dealing with preorders, incorporating subsort relations into the syntax of the language, and where formulas taking the third boolean value as interpretation contain a term or a predicate which is not well-sorted w.r.t. the signature. For this logic a ground tableau-based deduction method and a free variable extension version are proposed, proving their completeness.


Predicate Symbol Automate Theorem Prove Extension Rule Open Branch Expansion Rule 
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. [BG 95]
    L. Bachmair, H. Ganzinger, Ordered Chaining Calculi for First-Order Theories of Binary Relations. MPI-I-95-2-009, 1995.Google Scholar
  2. [BH 92]
    B. Beckert, R. Hähnle. An Improved Method for Adding Equality to Free Variable Semantic Tableaux. Proc. CADE'10. LNAI 607, 507–521, 1992.Google Scholar
  3. [BKS 85]
    W. W. Bledsoe, K. Kunen, R. Shostak. Completeness Results for Inequality Provers. Artificial Intelligence 27, 255–288, 1985.CrossRefGoogle Scholar
  4. [Fit 88]
    M. Fitting. First-Order modal tableaux. J. of Automated Reasoning 4, 191–213, 1988.Google Scholar
  5. [Fit 96]
    M. Fitting. First-Order Logic and Automated Theorem Proving. Second edition. Springer, 1996.Google Scholar
  6. [GL 90]
    A. Gavilanes-Franco, F. Lucio-Carrasco. A first order logic for partial functions. TCS 74, 37–69, 1990.Google Scholar
  7. [GLN 96]
    A. Gavilanes, J. Leach, S. Nieva. Free Variable Tableaux for a Many Sorted Logic with Preorders. To appear in Proc. AMAST'96, Springer, 1996.Google Scholar
  8. [GLMN 96]
    A. Gavilanes, J. Leach, P. J. Martín, S. Nieva. Reasoning with Preorders and Dynamic Sorts using Free Variable Tableaux. Technical Report DIA 34/96, Univ. Complutense de Madrid, 1996.Google Scholar
  9. [GM 92]
    J. A. Goguen, J. Meseguer. Order-sorted algebra I: Eguational deduction for multiple inheritance, overloading, exceptions and partial operations. TCS 105, 217–273, 1992.CrossRefGoogle Scholar
  10. [HS 94]
    R. Hähnle, P. H. Schmitt. The liberalized δ-rule in free variable semantic tableaux. J. of Automated Reasoning 13, 211–221, 1994.Google Scholar
  11. [JM 94]
    J. Jaffar, M. J. Maher. Constraint logic programming: A survey. J. of Logic Programming 19/20, 503–582, 1994.CrossRefGoogle Scholar
  12. [LA 93]
    J. Levy, J. Agustí. Bi-rewriting, a term rewriting technique for monotonie order relations. Proc. RTA'93. LNCS 690, 17–31, 1993.Google Scholar
  13. [LN 93]
    J. Leach, S. Nieva. Foundations of a Theorem Prover for Functional and Mathematical Uses. J. of Applied Non-Classical Logics 3(1), 7–38, 1993.Google Scholar
  14. [OS 88]
    F. Oppacher, E. Suen. HARP: A Tableau-Based Theorem Prover. J. of Automated Reasoning 4, 69–100, 1988.Google Scholar
  15. [Sch 89]
    M. Schmidt-Schauss. Computational aspects of an order sorted logic with term declarations. LNAI 395. Springer,1989.Google Scholar
  16. [SW 90]
    P.H. Schmitt, W. Wernecke. Tableau Calculus for Order Sorted Logic. Proc. Workshop on Sorts and Types in Artificial Intelligence (1989). LNAI 418, 49–60, 1990.Google Scholar
  17. [Wal 87]
    C. Walther. A Many-sorted Calculus based on Resolution and Paramodulation. Research Notes in Artificial Intelligence. Pitman, 1987.Google Scholar
  18. [Wal 90]
    C. Walther. Many Sorted Inferences in Automated Theorem Proving. Proc. Workshop on Sorts and Types in Artificial Intelligence (1989). LNAI 418, 18–48, 1990.Google Scholar
  19. [Wei 91]
    C. Weidenbach. A sorted logic using dynamic sorts. MPI-I-91-218, 1991.Google Scholar
  20. [Wei 95]
    C. Weidenbach. First-Order Tableaux with Sorts. J. of the Interest Group in Pure and Applied Logics 3(6), 887–907, 1995.Google Scholar
  21. [Wei]
    C. Weidenbach. Unification in Sort Theories and its Applications. Annals of Mathematics and Artificial Intelligence. To appear.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • A. Gavilanes
    • 1
  • J. Leach
    • 1
  • P. J. Martín
    • 1
  • S. Nieva
    • 1
  1. 1.Dep. de Informática y AutomáticaUniversidad Complutense de MadridSpain

Personalised recommendations