Presenting Intuitive Deductions via Symmetric Simplification

In automated deduction systems that are intended for human use, the presentation of a proof is no less important than its discovery. For most of today's automated theorem proving systems, this requires a non-trivial translation procedure to extract human-oriented deductions from machine-oriented proofs. Previously known translation procedures, though complete, tend to produce unintuitive deductions. One of the major flaws in such procedures is that too often the rule of indirect proof is

• Type: Conference
• Year: 1990
• Where: CADE
• Authors: Frank Pfenning, Dan Nesmith
• Keywords: Automated Theorem Proving, CADE 1990, Logical Reasoning, Non-trivial Translation Procedure, Translation Procedures