First-Order Tableaux with Sorts

Weidenbach, Christoph

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

First-Order Tableaux with Sorts

MPS-Authors

/persons/resource/persons45719

Weidenbach, Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Weidenbach, C. (1994). First-Order Tableaux with Sorts. In Broda, Krysia, D'Agostino, Marcello, & e. al. (Eds.), TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods (pp. 247-261). Imperial College of Science Technology and Medicine, TR-94/5.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-AD7C-5

Abstract

Tableau and the free variable tableau are extended with sorts. Sorts are sets of unary predicates. They can be attached to variables. Semantically, the domain of a variable is restricted to the intersection of the denotations of the attached predicates. Syntactically, the sort information is exploited by modified $\gamma$ and $\delta$ rules. The standard unification algorithm of free variable tableau is replaced by a sorted unification algorithm. The resulting calculi, tableau with sorts and free variable tableau with sorts are proved sound, complete and more suitable for mechanization than their counterparts without sorts.