Extracting the resolution algorithm from a completeness proof for the propositional calculus
From MaRDI portal
Publication:636273
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
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
Cites Work