[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Christoph Weidenbach
- First-Order Tableaux with Sorts
- Submitted to IGPL usenet group June 1995 ftp://dcs.ox.ac.uk/sorttab.ps.g(??)
- =THEORY LOGIC SEMANTIC TABLEAUX TREES TYPES
Gensen style natural induction (cf hodges) extended by adding sorts to variables,
- Each variable has a set of sorts assoicated with it.
- Each sort is interprtted as a unary predicate. s(x)=finite@(U->@)...
- for all x (p) +> for all x ( if and(s(x)(x)) then p).
- for some x (p) +> for some x ( and(s(x)(x)) and p).
Modified derivation rules
for all x (p(x)), and( s(x)(t) ), t any term|-P(t)
for some x (p(x)), new v|-p(v), and( s(x)(v) )
Gives much simpler proofs
Proved to be as complete and consistent as the original
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]