Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification

DOI10.1023/A:1005934721802zbMath0921.03012OpenAlexW1724004837MaRDI QIDQ1272615

Andrei Voronkov

Publication date: 29 September 1999

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1005934721802

zbMATH Keywords

automated theorem provinginstantiationderivation skeletonintuitionistic logic with equalitysimultaneous rigid \(E\)-unification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem ⋮ Proof-search in intuitionistic logic based on constraint satisfaction ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification