On the intuitionistic force of classical search (extended abstract)

DOI10.1007/3-540-61208-4_19zbMATH Open1415.03028OpenAlexW1587919740MaRDI QIDQ4645244FDOQ4645244

Authors: Eike Ritter, Lincoln Wallen, David Pym 

Publication date: 10 January 2019

Published in: Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61208-4_19

Recommendations

• On the intuitionistic force of classical search
• scientific article; zbMATH DE number 1390270
• Proof-terms for classical and intuitionistic resolution
• A proof-search procedure for intuitionistic propositional logic
• Proof-Search in Natural Deduction Calculus for Classical Propositional Logic

zbMATH Keywords

intuitionistic logicnatural deductionsequent calculusclassical logicproof procedure

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)

Cites Work

• Untersuchungen über das logische Schliessen. II
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Uniform proofs as a foundation for logic programming
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• Title not available (Why is that?)
• The correspondence between cut-elimination and normalization
• A Uniform Proof-theoretic Investigation of Linear Logic Programming
• First-order modal tableaux
• Title not available (Why is that?)
• Title not available (Why is that?)
• A note on the proof theory of the \(\lambda \Pi\)-calculus
• Title not available (Why is that?)

Cited In (11)

• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• On the intuitionistic force of classical search
• Title not available (Why is that?)
• Labelled proof systems for intuitionistic provability
• Proof-terms for classical and intuitionistic resolution
• Proof-terms for classical and intuitionistic resolution
• Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
• On the semantics of classical disjunction
• Proof-finding algorithms for classical and subclassical propositional logics
• A proof-search procedure for intuitionistic propositional logic
• Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them

Uses Software

• Automath

This page was built for publication: On the intuitionistic force of classical search (extended abstract)

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