Eigenvariables, bracketing and the decidability of positive minimal predicate logic

DOI10.1016/j.tcs.2006.01.053zbMath1106.03006OpenAlexW1988222104MaRDI QIDQ2503325

Ying Jiang, Gilles Dowek

Publication date: 14 September 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.01.053

zbMATH Keywords

sequent calculusdecidabilityminimal logicsystem Fbound variablepositive quantifier

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25)

Related Items (9)

How Hard Is Positive Quantification? ⋮ A unified procedure for provability and counter-model generation in minimal implicational logic ⋮ The existential fragment of second-order propositional intuitionistic logic is undecidable ⋮ Inhabitation of polymorphic and existential types ⋮ Proof Search and Counter Model of Positive Minimal Predicate Logic ⋮ Decidability of the Class E by Maslov’s Inverse Method ⋮ On the expressive power of schemes ⋮ On the Mints Hierarchy in First-Order Intuitionistic Logic ⋮ How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning

Cites Work

• Unnamed Item
• Unnamed Item
• Theorem proving modulo
• Sovability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers
• Contraction-free sequent calculi for intuitionistic logic
• Embedding first order predicate logic in fragments of intuitionistic logic
• Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic

This page was built for publication: Eigenvariables, bracketing and the decidability of positive minimal predicate logic