Semantic Foundations of Reductive Reasoning
Alexander V. Gheorghiu, David J. Pym
TL;DR
This paper develops the semantic foundations for reductive reasoning, a backward-inference paradigm that complements traditional deductive logic by focusing on reduction operators. It provides two complementary frameworks: a denotational semantics that models reduction operators as partial mappings to finite subgoals and a coinductive space of reductions, and an operational semantics based on GSOS that treats reductions as stateful transitions and supports large steps and composition. The authors connect reductive logic to proof-theoretic semantics (P-tS) and Milner’s tactical proof, showing that tactical proof arises naturally as an instance of P-tS for reductive reasoning. They also introduce the notion of control regimes to manage proof-search, discuss soundness and completeness relative to a base logic, and outline directions for handling information flow and proof plans in future work. The work provides a rigorous foundation for the semantic analysis of reduction and has implications for automated theorem proving, proof assistants, and practical problem-solving frameworks.
Abstract
The development of logic has largely been through the 'deductive' paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual 'reductive' perspective: collections of sufficient premisses are generated from putative conclusions. We call this paradigm, 'reductive logic'. This expression of logic encompass as diverse reasoning activities as proving a formula in a formal system to seeking to meet a friend before noon on Saturday. This paper is a semantical analysis of reductive logic. In particular, we provide mathematical foundations for representing and reasoning about 'reduction operators'. Heuristically, reduction operators may be thought of as `backwards' inference rules. In this paper, we address their mathematical representation, how they are used in the context of reductive reasoning, and, crucially, what makes them 'valid'.