Formalizing a hierarchical structure of practical mathematical reasoning

Robinson P.J. and Staples J. (1993) Formalizing a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3 1: 47-61. doi:10.1093/logcom/3.1.47


Author Robinson P.J.
Staples J.
Title Formalizing a hierarchical structure of practical mathematical reasoning
Journal name Journal of Logic and Computation   Check publisher's open access policy
ISSN 0955-792X
Publication date 1993-01-01
Sub-type Article (original research)
DOI 10.1093/logcom/3.1.47
Volume 3
Issue 1
Start page 47
End page 61
Total pages 15
Subject 1312 Molecular Biology
2613 Statistics and Probability
2605 Computational Mathematics
1708 Hardware and Architecture
1712 Software
2614 Theoretical Computer Science
2609 Logic
Abstract Traditionally, mathematical logic has been content with 'in principle' formalizations of deductive inference, which place little emphasis on the description of practical reasoning. Requirements for formal descriptions of practical inference methods are now emerging however. For example, interactive reasoning systems are needed for verification of computer systems, and should support practically convenient reasoning techniques as strongly as possible. This paper describes a proof paradigm which formalises a hierarchical, problem-reduction style of reasoning which is widely useful in practical reasoning. It is a goal directed paradigm, which gives a central role to equivalence transformations. A hierarchy of subgoals can co-exist at a single point in the proof, and these subgoals may be of arbitrary type. The approach allows good access to contextual information when transforming subgoals, and can be applied to a variety of logics.
Keyword Equivalence proofs
Inference systems
Interactive reasoning
Proof editors
Theorem provers
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status Unknown

Document type: Journal Article
Sub-type: Article (original research)
Collection: Scopus Import - Archived
 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 31 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Tue, 16 Aug 2016, 13:58:16 EST by System User