Presenting intuitive deductions via symmetric simplification

DOI10.1007/3-540-52885-7_98zbMath1509.68316MaRDI QIDQ6488543

Frank Pfenning, Dan Nesmith

Publication date: 28 April 2023

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

TPS: A hybrid automatic-interactive system for developing proofs ⋮ Reconstructing proofs at the assertion level

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On connections and higher-order logic
• A compact representation of proofs
• The translation of formal proofs into English
• Untersuchungen über das logische Schliessen. II
• Proofs as programs
• Bounds for proof-search and speed-up in the predicate calculus
• Some applications of Gentzen's proof theory in automated deduction
• The TPS theorem proving system

This page was built for publication: Presenting intuitive deductions via symmetric simplification