A Compressing Translation from Propositional Resolution to Natural Deduction

DOI10.1007/978-3-540-74621-8_6MaRDI QIDQ3525003zbMATH OpenOpenAlexFDO

Authors Hasan Amjad

Publication date 16 September 2008

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74621-8_6

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Propositional proof compressions and DNF logic
• Natural deduction in a paracomplete setting
• A logic program for transforming sequent proofs to natural deduction proofs
• Translations from natural deduction to sequent calculus
• Compression of propositional resolution proofs by lowering subproofs
• An alternative natural deduction for the intuitionistic propositional logic
• Compression of propositional resolution proofs via partial regularization
• Simplifying proofs in Fitch-style natural deduction systems
• Natural deduction for paraconsistent logic
• Proof-Search in Natural Deduction Calculus for Classical Propositional Logic

Cited in

(6)

• Translation of resolution proofs into short first-order proofs without choice axioms.
• Compressing propositional refutations
• Translation of resolution proofs into short first-order proofs without choice axioms
• Satisfiability modulo theories
• Data compression for proof replay
• Composition under distributive natural transformations: or, when predicate abstraction is impossible

Describes a project that uses

Uses Software

• HOL Light
• PVS

This page was built for publication: A Compressing Translation from Propositional Resolution to Natural Deduction

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