Reductive logic
Reductive logic is a paradigm of symbolic logic where rules in a Proof calculus and system are thought of as operators on the syntax via their reductive readings. Given a Proof calculus for a Mathematical logic and formal logic, reductive proofsearch is characterised precisely by the backward reading of rules in the calculus taking a putative conclusion to sufficient premises. The study of reductive logic aims to establish semantics (Denotational semantics and Operational semantics), for such procedures, and can therefore be regarded as the mathematical study of (reductive) proofsearch.
Concept
Logics are traditionally defined via a Formal language generated for grammar and an Mathematical induction defined Validity (logic)judgement acting as a calculus of inference.^{[1]} The inductive definition manifests the deductive paradigm of logic, where from established or supposed premises one proceeds to a conclusion, regulated by the application of inference rules e.g.,
<math>\Downarrow</math> 

A trace of inferences resulting is called a derivation, or a proof, of the last conclusion called the endsequent. In contrast, reductive inference proceeds from a putative (i.e., supposed) conclusion to sufficient premises, regulated by reduction operators,
<math>\Uparrow</math> 

Typically the reduction operators are the simply Admissible rule inferences applied in backward. The essential idea is summarised as follows:^{[2]}
 There is a logic <math>\mathcal{L}</math> with a proofsystem LL;
 We have a putative conclusion which is an assertion in <math>\mathcal{L}</math>, and we would like to know whether or not the sequent is provable in LL;
 Each inference rule LL, including any admissible rules, gives rise to a reduction operator. To apply a reduction operator to particular assertion we must find an instance of a reduction operator such that instance of the putative conclusion matches the assertion;
 The assertions which must be proved in order to have a proof of the initial assertion, or subgoals, are then given by the corresponding instances of the sufficient premises of the operator.
Reduction was first explained in these terms by Stephen Cole Kleene^{[3]}, but the first formal study of the subject in itself is attributed to a monograph by David Pym and Eike Ritter.^{[2]} Arguably the first theorems of reductive logic are Cutelimination theoremcutelimination for LK and LJ, and the various Completeness theoremcompleteness theorems of early formal logic.
Note, however, that a reduction may fail to yield a proof e.g., in LK one may encounter the sufficient premise <math>p \implies q</math>, for distinct atoms <math>p</math> and <math>q</math>. Such possible failures have no counterpart in deductive logic, but Automated theorem proving have to have strategies which ensure that a proof of a given endsequent is found if one exists. In general, not only the choice of reduction operators but also the order in which they are applied matters: the application of the same reduction operators in one order may yield a proof, where after applying the same reduction operators in a different order a completion to a proof may be impossible. As a consequence reductive logic has been characterised by the gestalt:^{[2]}
 Reductive Logic = Structure + Control
The structure component is the framework in which the proofsearch procedure is performed; and control is the mechanism for regulating the behaviour of the computation e.g, the disjunct to process, goal to reduce, clause to Resolution (logic)unify, or when to Backtracking. Majority of research has been focused on sequent calculi for Classical logic and Intuitionistic logicintuitionistic logic, particularly with respect to the structure component. The reductive logic of nonclassical logics e.g., Substructural logic, Bunched logic, and Modal logic, has not yet been studied; and no uniform mathematical background has been given for modelling control.
Motivation
Theorem proving, or algorithmic proofsearch, is both an essential enabling technology within the Computational science and of independent Philosophy and Mathematics interest. More specifically, in computing, many problems are formulated as judgements about formal texts, typical representable in logical formalisms. For example, wellformedness (parsing), welltypedness (Type checkingtypechecking), as well as logical consequence (e.g., for specification and correctness) itself.
There are many useful Formal language and, for each language, typically many useful procedures for judging properties of sentences. As the complexity of the languages and their properties increases, the possibility of obtaining efficient, Computability theory and total procedures recedes, but Computable function and partial procedures which fail quickly are of great value and Proof assistant and interactive theorem provers, such as the BoyerMoore theorem prover.BoyerMoore system,^{[4]} the LCF theorem proverLCF system and its derivatives,^{[5]} such Isabelle (proof assistant)Isabelle,^{[6]} as well as more complex systems, such as Coq,^{[7]} based on Dependent typedependent type theory, are used in a wide range of systemcritical applications.^{[8]}
Models
The inherent partiality of reductions presents a clear semantic difficulty i.e., how to interpret those reductions which cannot be completed to be proofs. Meanwhile, proofs as mathematical objects have been given general and rigours treatment though the CurryHowardLambek correspondence theorem: File:CurryHowardLambek_Correspondence.pdfcenterframeless331x331px The advantage is that proofs become subject to the mathematical tools developed in the corresponding formalisms e.g., they can be reasoned about as a arrows in a Category theorycategory. Research in reductive logic has largely focused on extending such models to the failed reductions.^{[2]}
Notes
 ↑ Dalen, D. van (Dirk), 1932 (2004). Logic and structure (4th ed.). Berlin: SpringerVerlag. ISBN 3540208798. OCLC 54529334.
{{cite book}}
: CS1 maint: multiple names: authors list (link)  ↑ ^{2.0} ^{2.1} ^{2.2} ^{2.3} Pym, David J. (2004). Reductive logic and proofsearch : proof theory, semantics, and control. Ritter, Eike. Oxford, UK: Clarendon Press. ISBN 0198526334. OCLC 54865392.
 ↑ Kleene, Stephen Cole, 19091994. (1967). Mathematical logic. New York. ISBN 0471490334. OCLC 523472.
{{cite book}}
: CS1 maint: multiple names: authors list (link)  ↑ Boyer, R. S.; Kaufmann, M.; Moore, J. S. (19950101). "The BoyerMoore theorem prover and its interactive enhancement". Computers & Mathematics with Applications. 29 (2): 27–62. doi:10.1016/08981221(94)002157. ISSN 08981221.
 ↑ Boyer, Robert S.; Moore, J Strother (1988), "Mechanized Proofs in the Logic", A Computational Logic Handbook, Elsevier, pp. 167–175, doi:10.1016/b9780121229528.50010x, ISBN 9780121229528
 ↑ Carbonell, Jaime G. (2002). Isabelle : a Proof Assistant for HigherOrder Logic. Springer Berlin Heidelberg. ISBN 9783540459491. OCLC 958524177.
 ↑ "Proof Search by Logic Programming", Certified Programming with Dependent Types, The MIT Press, 2013, doi:10.7551/mitpress/9153.003.0017, ISBN 9780262317870
 ↑ Schneier, Bruce. (2015). Secrets and lies : digital security in a networked world. John Wiley & Sons. ISBN 9781119092438. OCLC 911788931.
References
This article "Reductive logic" is from Wikipedia. The list of its authors can be seen in its historical. Articles taken from Draft Namespace on Wikipedia could be accessed on Wikipedia's Draft Namespace.
 Pym, David J. and Ritter, Eike (2004). "Reductive Logic and ProofSearch: Proof Theory, Semantics, and Control". Oxford University Press.