Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving (Q679252)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving |
scientific article; zbMATH DE number 1002306
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving |
scientific article; zbMATH DE number 1002306 |
Statements
Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving (English)
0 references
9 September 1997
0 references
In this paper two algorithms are presented for eliminating and introducing quantifiers without Skolemization of the wffs, and the unification theorem for them is proved. Using these algorithms the author has implemented an automatic natural deduction proving system. The Andrews challenge problem as well as the halting problem are proved by this system.
0 references
automated theorem proving
0 references
Gentzen system
0 references
unification algorithm
0 references
automatic natural deduction proving system
0 references
Andrews challenge problem
0 references
halting problem
0 references
0.826463520526886
0 references
0.7558306455612183
0 references
0.7419805526733398
0 references
