×

zbMATH — the first resource for mathematics

A resolution/tableaux algorithm for projective approximations in IPC. (English) Zbl 1005.03504
Summary: We present an algorithm, based both on semantic tableaux and resolution, which is able to check the projectivity (exactness) of a formula in intuitionistic propositional calculus. Suitably iterated, it also computes projective approximations, thus providing best E-unifiers for the equational theory of Heyting algebras. Applications to admissible inference rules are immediate.

MSC:
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI