[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

Weidenback94
  1. Christoph Weidenbach
  2. First-Order Tableaux with Sorts
  3. Submitted to IGPL usenet group June 1995 ftp://dcs.ox.ac.uk/sorttab.ps.g(??)
  4. =THEORY LOGIC SEMANTIC TABLEAUX TREES TYPES
      Gensen style natural induction (cf hodges) extended by adding sorts to variables,
    1. Each variable has a set of sorts assoicated with it.
    2. Each sort is interprtted as a unary predicate. s(x)=finite@(U->@)...
    3. for all x (p) +> for all x ( if and(s(x)(x)) then p).
    4. 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 uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]