Search

Your search keyword '"contraction-free"' showing total 7 results
Start Over Descriptor "contraction-free"
7 results on '"contraction-free"'

2. Contraction-free calculi for modal logics S5 and KD45

Author

Julius Andrikonis and Regimantas Pliuškevičius

Subjects
modal logic, sequent calculus, termination, backtracking, contraction-free, Mathematics, QA1-939
Abstract

It is known that termination and backtracking are among the most important problems in constructing derivations in non-classical logics. In this paper contractionfree and backtracking-free sequent calculi for modal logics S5 and KD45 are presented and founded. These are index-style sequent calculi with some specific indexed axioms. The main new ideas in considered calculi are to use metavariables (along with natural numbers) as elements of indexes and to numerate by different natural number all the positive occurrences of modality 2.

Published
2011
Full Text
View/download PDF

4. Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus

Author

Arisaka, Ryuta, Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, 000 Computer science, knowledge, general works, contraction-free, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], proof theory, cut elimination, Logic in Computer Science (cs.LO), Mathematics::Logic, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, sequent calculus, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, BI, Computer Science
Abstract

Development of a contraction-free BI sequent calculus, be the contraction-freeness implicit or explicit, has not been successful in the literature. We address this problem by presenting such a sequent system. Our calculus involves no structural rules. It should be an insight into non-formula contraction absorption in other non-classical logics. Contraction absorption in sequent calculus is associated to simpler cut elimination and to efficient proof searches.

Published
2014

5. Dubliavimo eliminavimas modalumo logikoms S5 ir KD45

Author

Regimantas Pliuškevičius and Julius Andrikonis

Subjects
termination, contraction-free, Backtracking, lcsh:Mathematics, Modal logic, Sequent calculus, Natural number, lcsh:QA1-939, backtracking, sequent calculus, Modal, Contraction-free, Termination, Calculus, Sequent, Contraction (operator theory), Axiom, modal logic, Mathematics
Abstract

It is known that termination and backtracking are among the most important problems in constructing derivations in non-classical logics. In this paper contractionfree and backtracking-free sequent calculi for modal logics S5 and KD45 are presented and founded. These are index-style sequent calculi with some specific indexed axioms. The main new ideas in considered calculi are to use metavariables (along with natural numbers) as elements of indexes and to numerate by different natural number all the positive occurrences of modality 2.

Published
2011

6. 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

7. 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