A Resolution/Tableaux Algorithm for Projective Approximations in IPC

DOI10.1093/jigpal/10.3.229zbMath1005.03504OpenAlexW2075172817MaRDI QIDQ3147430

Silvio Ghilardi

Publication date: 25 February 2003

Published in: Logic Journal of IGPL (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/jigpal/10.3.229

zbMATH Keywords

algorithmHeyting algebrasprojectivityresolutionequational theoryintuitionistic propositional calculusexact formulassemantic tableauxadmissible inference rulesE-unificationprojective approximations

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

On rules, A syntactic approach to unification in transitive reflexive modal logics, Tutorial on Admissible Rules in Gudauri, A Tableau Method for Checking Rule Admissibility in S4, Complexity of admissible rules, Unification, finite duality and projectivity in varieties of Heyting algebras, On unification and admissible rules in Gabbay-de Jongh logics, Best solving modal equations, Intermediate logics and Visser's rules, Unification in linear temporal logic LTL, On the rules of intermediate logics, Proof theory for admissible rules, DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV