•  30
    Simultaneous rigid sorted unification for tableaux
    with A. Gavilanes
    Studia Logica 72 (1): 31-59. 2002.
    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 the un…Read more
  •  5
    Free-variable tableaux for monotonic preorders
    with A. Gavilanes
    Logic Journal of the IGPL 9 (6): 813-844. 2001.