1,720,986 research outputs found
Semantic foundations of reductive reasoning
No full textThe 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
From proof-theoretic validity to base-extension semantics for intuitionistic propositional logic
No full textProof-theoretic semantics (P-tS) is the approach to meaning in logic based on proof (as opposed to truth). There are two major approaches to P-tS: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a semantics of arguments, and the latter is a semantics of logical constants. This paper demonstrates that the B-eS for intuitionistic propositional logic (IPL) encapsulates the declarative content of a version of P-tV based on the elimination rules. This explicates how the B-eS for IPL works, and shows the completeness of this version of P-tV.</p
Defining logical systems via algebraic constraints on proofs
No full textWe present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; e.g. one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of decomposition is to obtain a tool for uniform and modular treatment of proof theory and to provide a bridge between semantics logics and their proof theory. The paper discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics: including, a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic
Semantical Analysis of the Logic of Bunched Implications
No full textWe give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with eigenworlds (i.e., generic representatives of worlds) in an arbitrary model. This reasoning is captured by a sequent calculus for a meta-logic (in this case, first-order classical logic) expressive enough to capture the semantics of the object-logic. Essentially, one has a calculus of validity for the object-logic. The method proceeds through the perspective of reductive logic (as opposed to the more traditional paradigm of deductive logic), using the space of reductions as a medium for showing the behavioural equivalence of reduction in the sequent calculus for the object-logic and in the validity calculus. Rather than study the technique in general, we illustrate it for the logic of Bunched Implications (BI), thus IPL and MILL (without negation) are also treated. Intuitively, BI is the free combination of intuitionistic propositional logic and multiplicative intuitionistic linear logic, which renders its meta-theory is quite complex. The literature on BI contains many similar, but ultimately different, algebraic structures and satisfaction relations that either capture only fragments of the logic (albeit large ones) or have complex clauses for certain connectives (e.g., Beth’s clause for disjunction instead of Kripke’s). It is this complexity that motivates us to use BI as a case-study for this approach to semantics
Proof-theoretic semantics for intuitionistic multiplicative linear logic
No full textThis work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL). The starting point is a review of Sandqvist’s B-eS for intuitionistic propositional logic (IPL), for which we propose an alternative treatment of conjunction that takes the form of the generalized elimination rule for the connective. The resulting semantics is shown to be sound and complete. This motivates our main contribution, a B-eS for IMLL, in which the definitions of the logical constants all take the form of their elimination rule and for which soundness and completeness are established
Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
No full textThe reductive, as opposed to deductive, view of logic is the form of logic that is, perhaps, most widely employed in practical reasoning. In particular, it is the basis of logic programming. Here, building on the idea of uniform proof in reductive logic, we give a treatment of logic programming for BI, the logic of bunched implications, giving both operational and denotational semantics, together with soundness and completeness theorems, all couched in terms of the resource interpretation of BI’s semantics. We use this set-up as a basis for exploring how coalgebraic semantics can, in contrast to the basic denotational semantics, be used to describe the concrete operational choices that are an essential part of proof-search. The overall aim, toward which this paper can be seen as an initial step, is to develop a uniform, generic, mathematical framework for understanding the relationship between the deductive structure of logics and the control structures of the corresponding reductive paradigm
Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic
Full text linkProof-theoretic semantics (P-tS) is the paradigm of semantics in which
meaning in logic is based on proof (as opposed to truth). A particular instance
of P-tS for intuitionistic propositional logic (IPL) is its base-extension
semantics (B-eS). This semantics is given by a relation called support,
explaining the meaning of the logical constants, which is parameterized by
systems of rules called bases that provide the semantics of atomic
propositions. In this paper, we interpret bases as collections of definite
formulae and use the operational view of the latter as provided by uniform
proof-search -- the proof-theoretic foundation of logic programming (LP) -- to
establish the completeness of IPL for the B-eS. This perspective allows
negation, a subtle issue in P-tS, to be understood in terms of the
negation-as-failure protocol in LP. Specifically, while the denial of a
proposition is traditionally understood as the assertion of its negation, in
B-eS we may understand the denial of a proposition as the failure to find a
proof of it. In this way, assertion and denial are both prime concepts in P-tS.Comment: submitte
Investigations into Semantics in Reductive Logic
Full text linkLogic is the study of reasoning. Typically, it proceeds in terms of inferring a conclusion from established premises. The systematic use of symbolic and mathematical techniques to determine the forms of valid reasoning on this plan determines Deductive Logic. Reductive Logic is the dual paradigm that proceeds by generating from a putative conclusion a set of sufficient premises. While logical consequence
can be characterized through proof-theoretic and semantic approaches, work in Reductive Logic has traditionally focused on the former. This monograph is composed of three parts that illustrate the interplay between semantics and proof in Reductive
Logic: Part I comprises a case-study, Part II develops tools and gives result for a more general account, and Part III considers a semantics entirely based on notions of proofs. These a briefly outlined below.
In Part I, the monograph examines proof-search in the logic of Bunched Implications (BI), presenting technical results such as cut-elimination, logic programming, and focusing. It also illustrates a novel approach to soundness and complete-
ness (S&C) for BI that proceeds entirely through proof-search methods, eliminating the need for constructing term- and counter-models.
In Part II, the monograph introduces and develops the theory of a paradigm of proof system called ‘algebraic constraint systems’ (ACSs). Briefly, ACSs are
sequent calculi enriched with an algebra over which constraints are generated during reduction that, when solved, determine a proof. They help bridge the gap between proof theory and semantics in Reductive Logic. In particular, the part uses ACSs for
the following: to provide a general account of the approach to S&C studied in BI; to systematically generate relational calculi for logics that satisfy specific conditions; and to derive a semantics of IPL from its proof theory.
In Part III, the monograph explores proof-theoretic semantics — the approach to meaning in logic based on proof rather than truth — and provides both general insights and a range of technical results.
While the monograph contains several contributions to logic across mathematics, informatics, and philosophy, its real contribution is to demonstrate the viability and merit of studying semantics from the perspective of Reductive Logic and to give methods, techniques, and tools for a systematic theory to be developed
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
