Automated proof construction in type theory using resolution
From MaRDI portal
Publication:1868508
DOI10.1023/A:1021939521172zbMath1015.03018OpenAlexW2168281995MaRDI QIDQ1868508
Hans de Nivelle, Dimitri Hendriks, Marc Bezem
Publication date: 27 April 2003
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1021939521172
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items
Hammer for Coq: automation for dependent type theory, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, Automation for interactive proof: first prototype, On the mechanization of the proof of Hessenberg's theorem in coherent logic, Translation of resolution proofs into short first-order proofs without choice axioms, Extending Sledgehammer with SMT Solvers, Lightweight relevance filtering for machine-generated resolution problems, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Extending Sledgehammer with SMT solvers
Uses Software
