A Resolution/Tableaux Algorithm for Projective Approximations in IPC

DOI10.1093/JIGPAL/10.3.229MaRDI QIDQ3147430zbMATH OpenOpenAlexFDO

Authors Silvio Ghilardi

Publication date 25 February 2003

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

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

zbMATH Keywords

algorithmresolutionprojectivityHeyting algebrassemantic tableauxequational theoryadmissible inference rulesexact formulasE-unificationintuitionistic propositional calculusprojective approximations

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• A resolution theorem prover for intuitionistic logic
• Anti-chains, focuses and projective formulas
• Computer Science Logic
• scientific article; zbMATH DE number 1341466
• scientific article; zbMATH DE number 4130350

Cited in

(19)

• A tableau method for checking rule admissibility in S4
• Unification in linear temporal logic LTL
• On rules
• A syntactic approach to unification in transitive reflexive modal logics
• On unification and admissible rules in Gabbay-de Jongh logics
• DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV
• Intermediate logics and Visser's rules
• Unification, finite duality and projectivity in varieties of Heyting algebras
• Complexity of admissible rules
• Proof theory for admissible rules
• Undecidability of admissibility in the product of two \textbf{Alt} logics
• Best solving modal equations
• On the rules of intermediate logics
• Relative unification in intuitionistic logic: towards the provability logic of HA
• Anti-chains, focuses and projective formulas
• Tutorial on admissible rules in Gudauri
• Computing most general unifiers in Euclidean modal logics
• Investigating definability in propositional logic via sheaves on Grothendieck topologies
• On the theory of epistemic Łukasiewicz logic corresponding to the Chang algebra with application in immune system

This page was built for publication: A Resolution/Tableaux Algorithm for Projective Approximations in IPC

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3147430)