Search

Your search keyword '"contraction-free"' showing total 2 results
Start Over Descriptor "contraction-free" Topic 0102 computer and information sciences
2 results on '"contraction-free"'

1. A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic

Author

Brian Hill, Francesca Poggiolesi, Groupement de Recherche et d'Etudes en Gestion à HEC (GREGH), Ecole des Hautes Etudes Commerciales (HEC Paris)-Centre National de la Recherche Scientifique (CNRS), Vrije Universiteit Brussel (VUB), Institut d'Histoire et de Philosophie des Sciences et des Techniques (IHPST), Université Paris 1 Panthéon-Sorbonne (UP1)-Département d'Etudes Cognitives - ENS Paris (DEC), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-École normale supérieure - Paris (ENS Paris), and Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Contraction-free, Propositional Dynamic Logic, Logic, Cut-elimination theorem, Zeroth-order logic, 0102 computer and information sciences, 01 natural sciences, History and Philosophy of Science, Proof calculus, [SHS.ECO.ECO]Humanities and Social Sciences/Economics and Finance/domain_shs.eco.eco, Computer Science::Logic in Computer Science, Tree-hypersequent, Calculus, [INFO]Computer Science [cs], Sequent, 0101 mathematics, Mathematics, Propositional variable, Discrete mathematics, Natural deduction, 010102 general mathematics, Noncommutative logic, Proof theory, [SHS.PHIL]Humanities and Social Sciences/Philosophy, Sequent calculus, Mathematics::Logic, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Cut-free
Abstract

International audience; In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infini-tary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.

Published
2010

2. The Method of Tree-Hypersequents for Modal Propositional Logic

Author

Francesca Poggiolesi, Institut d'Histoire et de Philosophie des Sciences et des Techniques (IHPST), Université Paris 1 Panthéon-Sorbonne (UP1)-Département d'Etudes Cognitives - ENS Paris (DEC), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS), David Makinson, Jacek Malinowski, and Heinrich Wansing

Subjects
Hypersequents, Contraction-free, Discrete mathematics, Propositional variable, Natural deduction, Cut-elimination theorem, Normal modal logic, Modal logic, 010102 general mathematics, Modal μ-calculus, Sequent calculus, 0102 computer and information sciences, 16. Peace & justice, 01 natural sciences, [SHS.HISPHILSO]Humanities and Social Sciences/History, Philosophy and Sociology of Sciences, Sequent Calculus, 010201 computation theory & mathematics, Cut-free, Calculus, Sequent, 0101 mathematics, Tree-hypersequents, Mathematics
Abstract

Paper from the Studia Logica conference Trends in Logic IV; In this paper we present a method, that we call the tree-hypersequent method, for generating contraction-free and cut-free sequent calculi for modal propositional logics. We show how this method works for the systems K, KD, K4 and KD4, by giving a sequent calculus for these systems which are normally presented in the Hilbert style, and by proving all the main results in a purely syntactical way.

Published
2008

Catalog

Books, media, physical & digital resources
See catalog results