Double-negation elimination in some propositional logics

DOI10.1007/s11225-005-8469-4zbMath1086.03046arXivcs/0301026OpenAlexW2011672095WikidataQ114262834 ScholiaQ114262834MaRDI QIDQ813082

Larry Wos, Robert Veroff, Michael J. Beeson

Publication date: 30 January 2006

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/cs/0301026

zbMATH Keywords

automated reasoningintuitionistic logiccondensed detachmentclassical propositional calculusexistence of axiom systemexistence of proofs free of double negationinfinite-valued sentential calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05) Structure of proofs (03F07) Many-valued logic (03B50) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (1)

Larry Wos: visions of automated reasoning

Uses Software

• OTTER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Condensed detachment is complete for relevance logic: A computer-aided proof
• The resonance strategy
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• Notes on the axiomatics of the propositional calculus
• Bounded contraction and Gentzen-style formulation of Łukasiewicz logics
• Algebraic Analysis of Many Valued Logics
• Fragments of Many-Valued Statement Calculi
• Principal type-schemes and condensed detachment
• A Fascinating Country in the World of Computing
• A Machine-Oriented Logic Based on the Resolution Principle
• The separation theorem of intuitionist propositional calculus
• A legacy recalled and a tradition continued
• Conquering the Meredith single axiom
• Finding missing proofs with automated reasoning

This page was built for publication: Double-negation elimination in some propositional logics