Long normal form proof search and counter-model generation

MaRDI QIDQ2703714zbMATH OpenFDO

Authors Sachio Hirokawa, Daisuke Nagano

Publication date 7 May 2001

zbMATH Keywords

intuitionistic logiclambda-calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Proof Search and Counter Model of Positive Minimal Predicate Logic
• Proof finding algorithms for implicational logics
• Mechanizing Mathematical Reasoning
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• A proof-search procedure for intuitionistic propositional logic

Cited in

(4)

• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• A unified procedure for provability and counter-model generation in minimal implicational logic
• Intuitionistic games: determinacy, completeness, and normalization
• Proof Search and Counter Model of Positive Minimal Predicate Logic

Describes a project that uses

Uses Software

• STRIP

This page was built for publication: Long normal form proof search and counter-model generation

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