Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification (Q1272615): Difference between revisions
From MaRDI portal
Removed claim: reviewed by (P1447): Item:Q583186 |
Set OpenAlex properties. |
||
(2 intermediate revisions by 2 users not shown) | |||
Property / reviewed by | |||
Property / reviewed by: N. K. Zamov / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1023/a:1005934721802 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1724004837 / rank | |||
Normal rank |
Latest revision as of 10:10, 30 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification |
scientific article |
Statements
Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification (English)
0 references
29 September 1999
0 references
In automated theorem proving methods the variable instantiation during proof search is usually controlled by a suitable unification algorithm. The author presents some analysis of the instantiation problem for intuitionistic logic with equality. This analysis shows close connections between variable instantiation problem and simultaneous rigid \(E\)-unification. It implies that simultaneous rigid \(E\)-unification is unavoidable in automatic proof procedures for intuitionistic logic with equality. Using a description of provability in terms of a derivation skeleton and constraints, the author shows that the existence of a derivation with a given skeleton is polynomial-time equivalent to simultaneous rigid \(E\)-unifiability. The author also shows that simultaneous rigid \(E\)-unifiability is polynomial-time reducible to intuitionistic logic with equality. These two facts show that a semi-decision algorithm for simultaneous rigid \(E\)-unifiability is necessary and sufficient for designing automated theorem-proving procedures for intuitionistic logic with equality.
0 references
automated theorem proving
0 references
instantiation
0 references
intuitionistic logic with equality
0 references
simultaneous rigid \(E\)-unification
0 references
derivation skeleton
0 references