Proof-terms for classical and intuitionistic resolution

DOI10.1093/LOGCOM/10.2.173MaRDI QIDQ4487255zbMATH OpenOpenAlexFDO

Authors Eike Ritter, Lincoln Wallen, David Pym

Publication date 4 September 2000

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/a17cb95bdcde8133c8a6ec9949ebed1774dd7135

zbMATH Keywords

automated deductionclassical logicintuitionistic logiclambda calculusproof-searchresolutiontheorem-proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• Proof-terms for classical and intuitionistic resolution
• On the intuitionistic force of classical search
• scientific article; zbMATH DE number 2095713
• On the intuitionistic force of classical search (extended abstract)
• scientific article; zbMATH DE number 4027425

Cited in

(4)

• On the intuitionistic force of classical search
• Correspondences between classical, intuitionistic and uniform provability
• Proof-search in type-theoretic languages: An introduction
• Proof-terms for classical and intuitionistic resolution

This page was built for publication: Proof-terms for classical and intuitionistic resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4487255)