Search

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

The paper treats 4 different fragments of first-order logic induced by their respective versions of Kripke style semantics for modal intuitionistic logic. In order to capture these fragments, the notion of asimulation is modified and extended to yield Van Benthem type of semantic characterization of their respective expressive powers. It is shown, further, that this characterization can be easily carried over to arbitrary first-order definable subclasses of classical first-order models., Comment: 29 pages, 0 figures. arXiv admin note: text overlap with arXiv:1207.4414

Combinatorial proofs are abstract invariants for sequent calculus proofs, similarly to homotopy groups which are abstract invariants for topological spaces. Sequent calculus fails to be surjective onto combinatorial proofs, and here we extract a syntactically motivated closure of sequent calculus from which there is a surjection onto a complete set of combinatorial proofs. We characterize a class of canonical sequent calculus proofs for the full set of propositional tautologies and derive a new completeness theorem for combinatorial propositions. For this, we define a new mapping between combinatorial proofs and sequent calculus proofs, different from the one originally proposed, which explicitly links the logical flow graph of a proof to a skew fibration between graphs of formulas. The categorical properties relating the original and the new mappings are explicitly discussed.

Bu tez temel olarak cebirsel yapılar ve önermeler lojiği arasındaki bağlantı ile ilgilidir. Grupların, halkaların, cebirlerin, R-modüllerin ve kafeslerin tanımları verilmiş ve önermeler lojiği ile arasında bağlantı kurulmuştur. Özellikle kafes teorisi ve cebirler üzerinde durulmuştur. Bunun yanısıra bazı sonlu teorilerin kardinalleri üzerinde çalışılmıştır. This thesis is mainly concerned with the relationship between algebraic structures and propotisional logic. Basic definitions of groups, ring, lattices, algebras and R-modules are presented and the relationship between they and propositional logic are established. Specially lattice theory and algebras are emphasized. In additional to , the cardinalty of some finite theories are studied. 92

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean theory and show that each of them gives rise to a Boolean decision procedure based on a canonical rewrite system modulo associativity and commutativity. Then, we present two modular extensions of our decision procedure for Dijkstra-Scholten propositional logic to the Sequent Calculus for First Order Logic and to the Syllogistic Logic with Complements of L. Moss. These extensions take the form of rewrite theories that are sound and complete for performing deduction modulo their equational parts and exhibit good mechanization properties. We illustrate the practical usefulness of this approach by a direct implementation of one of these theories in Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving., Deducción con reglas de inferencia Las reglas de cálculo del módulo juegan un papel importante en la deducción automatizada como un método eficaz para escalar. Presentamos cuatro teorías ecuacionales que son isomorfas a la teoría booleana tradicional y mostramos que cada una de ellas da lugar a un procedimiento de decisión booleano basado en un sistema canónico de reescritura módulo asociatividad y conmutatividad. Luego, presentamos dos extensiones modulares de nuestro procedimiento de decisión para la lógica proposicional de Dijkstra-Scholten al Cálculo Secuente para Lógica de Primer Orden ya la Lógica Silogística con Complementos de L. Moss. Estas extensiones toman la forma de teorías de reescritura que son sólidas y completas para realizar la deducción módulo de sus partes ecuacionales y exhiben buenas propiedades de mecanización. Ilustramos la utilidad práctica de este enfoque mediante una implementación directa de una de estas teorías en Maude, reescribiendo el lenguaje lógico y demostrando automáticamente un punto de referencia de desafío en la demostración de teoremas.

In this note we compare propositional logics for closed substitutions and propositional logics for open substitutions in constructive arithmetical theories. We provide a strong example where these logics diverge in an essential way. We prove that for Markov's Arithmetic, that is, Heyting's Arithmetic plus Markov's principle plus Extended Church's Thesis, the logic of closed and the logic of open substitutions are the same.

In this paper the correspondence between safe Petri nets and event structures, due to Nielsen, Plotkin and Winskel, is extended to arbitrary nets without self-loops, under the collective token interpretation. To this end we propose a more general form of event structure, matching the expressive power of such nets. These new event structures and nets are connected by relating both notions with configuration structures, which can be regarded as representations of either event structures or nets that capture their behaviour in terms of action occurrences and the causal relationships between them, but abstract from any auxiliary structure. A configuration structure can also be considered logically, as a class of propositional models, or - equivalently - as a propositional theory in disjunctive normal from. Converting this theory to conjunctive normal form is the key idea in the translation of such a structure into a net. For a variety of classes of event structures we characterise the associated classes of configuration structures in terms of their closure properties, as well as in terms of the axiomatisability of the associated propositional theories by formulae of simple prescribed forms, and in terms of structural properties of the associated Petri nets., Contributed to the Festschrift for Mogens Nielsen's 60th birthday

Prior to investigating the degree of maximality of a propositional logic, as is the notion introduced by Ryszard Wójcicki [8], it is important to determine all structural consequence stronger than the logic considered. This characterization of all structural strengthenings was performed while establishing the degree of maximality for Lukasiewicz and Lukasiewicz-like logics [8], [4], [9], [5]. In these papers the authors used matrix consequences together with certain results concerning this notion and a representation theorem for Lukasiewicz algebras as given by R. S. Grigolia [2] (Fragment tekstu).