Academic
Publications
A Science of Reasoning

A Science of Reasoning,Alan Bundy

A Science of Reasoning   (Citations: 77)
BibTex | RIS | RefWorks Download
This paper addresses the question of how we can understand reasoning in general andmathematical proofs in particular. It argues the need for a high-level understanding ofproofs to complement the low-level understanding provided by Logic. It proposes a role forcomputation in providing this high-level understanding, namely by the association of proofplans with proofs. Proof plans are defined and examples are given for two families of proofs.Criteria are given for assessing the...
Conference: Birthday ... , pp. 178-198, 1991
Cumulative Annual
    • ...This incremental approach is already used in the construction of proof plans [9], i.e...
    • ...For instance the granularity of the proof steps plays a very important role in this sense [9]...
    • ...Thus this representation appears more suitable than the previous one for highlighting the algorithmic parts of proofs [16], for retrieving common patterns in the structure of proofs [9], and for evolving proofs...
    • ...This means that advanced tactics with a formal semantics must be provided (see [9] for some examples of such...

    Ferruccio Guidi. Procedural Representation of CIC Proof Terms

    • ...1. Construct a proof plan [3] that can be used to identify the information required to solve the current problem and then solve it. 2. Retrieve this information and use it to construct an initial problem-specific, logic-based ontology from multiple sources...

    Jonathan A. Abourbihet al. A Single-Significant-Digit Calculus for Semi-Automated Guesstimation

    • ...see the proof plan data structure PDS [7, 22] in mega [4, 56] or high-level proofs in [13]), or request the system to print all steps, declarations, and denitions...

    Cristian S. Caludeet al. Formal Proof: Reconciling Correctness and Understanding

    • ...ΩMEGA’s main focus is on knowledge-based proof planning [24, 25, 66, 70], where proofs are not conceived in terms of low-level calculus rules, but at a less detailed granularity, that is at a more abstract level, that highlights the main ideas and deemphasises minor logical or mathematical manipulations of formulas...

    Serge Autexieret al. ΩMEGA: Resource-Adaptive Processes in an Automated Reasoning System

    • ...– Problems 1 and 2 are being addressed by developing repair plans .Ar epair plan is analogous to a proof plan [5], a generic proof outline that can be used to guide the search for a proof...

    Alan Bundyet al. Towards Ontology Evolution in Physics

Sort by: