Two loop detection mechanisms: A comparison

DOI10.1007/BFb0027414zbMath1412.68234OpenAlexW1874611656MaRDI QIDQ4610326

Jacob M. Howe

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0027414

zbMATH Keywords

theorem provingsequent calculusintuitionistic logicproof treepropositional variable

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (7)

A unified procedure for provability and counter-model generation in minimal implicational logic ⋮ Proof theory for positive logic with weak negation ⋮ Unnamed Item ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ A coinductive approach to proof search through typed lambda-calculi ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models

Uses Software

• SICStus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• A new constructive logic: classic logic
• Contraction-free sequent calculi for intuitionistic logic
• Efficient loop-check for backward proof search in some non-classical propositional logics
• A resolution theorem prover for intuitionistic logic
• An Intuitionistic Predicate Logic Theorem Prover

This page was built for publication: Two loop detection mechanisms: A comparison