Extracting the resolution algorithm from a completeness proof for the propositional calculus

DOI10.1016/j.apal.2009.07.008zbMath1221.03015OpenAlexW2022840750MaRDI QIDQ636273

Wojciech Moczydłowski, Robert L. Constable

Publication date: 26 August 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://hdl.handle.net/1813/5754

zbMATH Keywords

automated reasoningresolutionprogram extractiontype theoryCoqintuitionismHaskell program

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05)

Related Items

On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic, Completeness in PVS of a nominal unification algorithm

Uses Software

• Coq
• Haskell
• SATCHMO
• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Model theory
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• The Completeness of Propositional Resolution: A Simple and Constructive Proof
• A Machine-Oriented Logic Based on the Resolution Principle