Comparing approaches to resolution based higher-order theorem proving (Q1868166): Difference between revisions
From MaRDI portal
Created a new Item |
Set profile property. |
||
(5 intermediate revisions by 3 users not shown) | |||
Property / reviewed by | |||
Property / reviewed by: N. K. Zamov / rank | |||
Property / reviewed by | |||
Property / reviewed by: N. K. Zamov / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: TPS / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: Leo / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 06:00, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Comparing approaches to resolution based higher-order theorem proving |
scientific article |
Statements
Comparing approaches to resolution based higher-order theorem proving (English)
0 references
27 April 2003
0 references
Four approaches to resolution-based higher-order theorem proving are investigated: Andrews' higher-order resolution approach; Huet's constrained resolution approach; higher-order E-resolution; and extensional higher-order resolution. The author focuses on Henkin completeness and full extensionality. The paper demonstrates that simply adding extensionality axioms to the search space increases the amount of blind search. Higher-order E-unification and R-resolution improves the situation but it does still not provide a general solution. Extensional higher-order resolution is the sole studied approach that can completely avoid the extensionality axioms.
0 references
higher-order logic
0 references
higher-order resolution
0 references
resolution-based higher-order theorem proving
0 references
Henkin completeness
0 references
full extensionality
0 references