Electronic Resource
Springer
Journal of automated reasoning
3 (1987), S. 225-246
ISSN:
1573-0670
Keywords:
Theorem proving
;
semantic tableaux
;
first-order logic with equality
;
partial unification
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract An extension to the system of semantic tableaux to deal with first-order logic with equality is introduced and proved sound and complete. This involves the use of partial unification, an operation which is based on unification without the presence of variables. We show, further, that semantic tableaux with partial unification provide a sound and complete proof method without needing the functionally reflexive axioms. We also give an example of an ordering rule which allows us to provide less complex proofs in the ground case.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00243790
Permalink
| Library |
Location |
Call Number |
Volume/Issue/Year |
Availability |
