scientific article; zbMATH DE number 1292293

MaRDI QIDQ4244301zbMATH OpenFDO

Authors Oliver Bittel

Publication date 27 May 1999

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 52087
• Mechanical procedure for proof construction via closed terms in typed calculus
• \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
• Automated synthesis of tableau calculi
• A resolution theorem prover for intuitionistic logic

Cited in

(13)

• Representing scope in intuitionistic deductions
• Proof-search in type-theoretic languages: An introduction
• lean\(T^ AP\): Lean tableau-based deduction
• Automata theory approach to predicate intuitionistic logic
• Simplification Rules for Intuitionistic Propositional Tableaux
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• scientific article; zbMATH DE number 52087 (Why is no real title available?)
• scientific article; zbMATH DE number 1231697 (Why is no real title available?)
• Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
• scientific article; zbMATH DE number 5592264 (Why is no real title available?)
• Automated synthesis of tableau calculi
• A higher-order interpretation of deductive tableau
• Interpolation theorems for intuitionistic predicate logic

This page was built for publication:

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