Switch to: References

Add citations

You must login to add citations.
  1. Simultaneous rigid sorted unification for tableaux.P. J. Martín & A. Gavilanes - 2002 - Studia Logica 72 (1):31-59.
    In this paper we integrate a sorted unification calculus into free variable tableau methods for logics with term declarations. The calculus we define is used to close a tableau at once, unifying a set of equations derived from pairs of potentially complementary literals occurring in its branches. Apart from making the deduction system sound and complete, the calculus is terminating and so, it can be used as a decision procedure. In this sense we have separated the complexity of sorts from (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Order-sorted logic programming with predicate hierarchy.Ken Kaneiwa - 2004 - Artificial Intelligence 158 (2):155-188.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Limited reasoning in first-order knowledge bases with full introspection.Gerhard Lakemeyer - 1996 - Artificial Intelligence 84 (1-2):209-255.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • A typed resolution principle for deduction with conditional typing theory.Tie-Cheng Wang - 1995 - Artificial Intelligence 75 (2):161-194.
    Download  
     
    Export citation  
     
    Bookmark  
  • A resolution principle for constrained logics.Hans-Jürgen Bürckert - 1994 - Artificial Intelligence 66 (2):235-271.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Hybrid reasoning using universal attachment.Karen L. Myers - 1994 - Artificial Intelligence 67 (2):329-375.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Theorem proving with built-in hybrid theories.Uwe Petermann - 1998 - Logic and Logical Philosophy 6:77.
    A growing number of applications of automated reasoning exhibitsthe necessity of flexible deduction systems. A deduction system should beable to execute inference rules which are appropriate to the given problem.One way to achieve this behavior is the integration of different calculi. Thisled to so called hybrid reasoning [22, 1, 10, 20] which means the integrationof a general purpose foreground reasoner with a specialized background reasoner. A typical task of a background reasoner is to perform special purposeinference rules according to a (...)
    Download  
     
    Export citation  
     
    Bookmark