Proof-terms for classical and intuitionistic resolution

DOI10.1093/logcom/10.2.173zbMath0958.03012OpenAlexW1993039936MaRDI QIDQ4487255

Lincoln Wallen, Eike Ritter, David J. 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

resolutionintuitionistic logiclambda calculusclassical logicautomated deductiontheorem-provingproof-search

Mathematics Subject Classification ID

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

Related Items (3)

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

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