Maximum Cuts in Extended Natural Deduction

Mirjana Borisavljević

Displaying similar documents to “Maximum Cuts in Extended Natural Deduction”

Connections between cuts and maximum segments

Mirjana Borisavljević (2010)

Kragujevac Journal of Mathematics

Similarity:

Normalization as a consequence of cut elimination

Mirjana Borisavljević (2009)

Publications de l'Institut Mathématique

Similarity:

Minimum segments in sequent derivations.

Borisavljević, Mirjana (2003)

Publications de l'Institut Mathématique. Nouvelle Série

Similarity:

Normal Form Theorem for Systems of Sequents

Mirjana Borisavljević (2007)

Publications de l'Institut Mathématique

Similarity:

A Parigot-style linear $λ$ -calculus for full intuitionistic linear logic.

de Paiva, Valeria, Ritter, Eike (2006)

Theory and Applications of Categories [electronic only]

Similarity:

Strong normalization proofs for cut elimination in Gentzen's sequent calculi

Elias Bittar (1999)

Banach Center Publications

Similarity:

We define an equivalent variant $L K_{s p}$ of the Gentzen sequent calculus $L K$ . In $L K_{s p}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $_{L K_{s p}}$ by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation;...

The Derivations of Temporal Logic Formulas

Mariusz Giero (2012)

Formalized Mathematics

Similarity:

This is a preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [12]. We introduce n-ary connectives and prove their properties. We derive temporal logic formulas.

Generators of rings of constants of derivations.

Jȩdrzejewicz, Piotr (2007)

Zeszyty Naukowe Uniwersytetu Jagiellońskiego. Universitatis Iagellonicae Acta Mathematica

Similarity:

Weak Completeness Theorem for Propositional Linear Time Temporal Logic

Mariusz Giero (2012)

Formalized Mathematics

Similarity:

We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator. We base it on the proof of completeness for basic propositional linear time temporal logic given in [20] which roughly follows the idea of the Henkin-Hasenjaeger method for classical logic. We show that a temporal model exists for every formula which negation is not derivable (Satisfiability Theorem). The contrapositive of that...

Computational Interrpretations of Logics

Silvia Ghilezan, Silvia Likavec (2009)

Zbornik Radova

Similarity:

Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem

Marco Caminati (2011)

Formalized Mathematics

Similarity:

Fifth of a series of articles laying down the bases for classical first order model theory. This paper presents multiple themes: first it introduces sequents, rules and sets of rules for a first order language L as L-dependent types. Then defines derivability and provability according to a set of rules, and gives several technical lemmas binding all those concepts. Following that, it introduces a fixed set D of derivation rules, and proceeds to convert them to Mizar functorial cluster...