Tableau methods for a logic with term declarations

Authors
Martin, PJ Gavilanes, A Leach, J
Citation
Pj. Martin et al., Tableau methods for a logic with term declarations, J SYMB COMP, 29(2), 2000, pp. 343-372
Citations number
13
Categorie Soggetti
Engineering Mathematics
Journal title
JOURNAL OF SYMBOLIC COMPUTATION
ISSN journal
07477171 → ACNP
Volume
29
Issue
2
Year of publication
2000
Pages
343 - 372
Database
ISI
SICI code
0747-7171(200002)29:2<343:TMFALW>2.0.ZU;2-8
Abstract
We study free variable tableau methods for logics with term declarations. W e show how to define a substitutivity rule preserving the soundness of the tableaux and we prove that some other attempts lead to unsound systems. Bas ed on this rule, we define a sound and complete free variable tableau syste m and we show how to restrict its application to close branches by defining a sorted unification calculus. (C) 2000 Academic Press.