Zobrazeno 1 - 10
of 102
pro vyhledávání: '"Strassburger, Lutz"'
Autor:
Straßburger, Lutz
The news we consume influence our political opinions, and therefore whoever controls which news we read also controls our political opinions. Does this mean that the algorithms that select our news determine the outcomes of our elections?
Externí odkaz:
http://arxiv.org/abs/2402.03409
Publikováno v:
The Art, Science, and Engineering of Programming, 2024, Vol. 8, Issue 1, Article 3
A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the CompCert project,
Externí odkaz:
http://arxiv.org/abs/2306.12411
Publikováno v:
Proceedings of LICS 2023 (2023)
In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson's PhD thesis in 1994. We obtain thi
Externí odkaz:
http://arxiv.org/abs/2304.12094
Publikováno v:
Logical Methods in Computer Science, Volume 19, Issue 4 (December 18, 2023) lmcs:10057
Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV originates fro
Externí odkaz:
http://arxiv.org/abs/2209.07825
We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof system based on inference rules, a combinatorial proof is a syntax-free
Externí odkaz:
http://arxiv.org/abs/2104.13124
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a
Externí odkaz:
http://arxiv.org/abs/2104.09115
Publikováno v:
Logical Methods in Computer Science, Volume 18, Issue 4 (October 21, 2022) lmcs:6957
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we
Externí odkaz:
http://arxiv.org/abs/2012.01102
Autor:
Das, Anupam, Straßburger, Lutz
Publikováno v:
Logical Methods in Computer Science, Volume 12, Issue 4 (April 27, 2017) lmcs:2621
Linear rules have played an increasing role in structural proof theory in recent years. It has been observed that the set of all sound linear inference rules in Boolean logic is already coNP-complete, i.e. that every Boolean tautology can be written
Externí odkaz:
http://arxiv.org/abs/1610.08772
Autor:
Straßburger, Lutz
Les questions "Qu'est-ce qu'une preuve?" et "Quand deux preuves sont-elles identiques?" sont fondamentales pour la théorie de la preuve. Mais pour la logique classique propositionnelle --- la logique la plus répandue --- nous n'avons pas encore d
Externí odkaz:
http://tel.archives-ouvertes.fr/tel-00772590
http://tel.archives-ouvertes.fr/docs/00/77/25/90/PDF/thehabil.pdf
http://tel.archives-ouvertes.fr/docs/00/77/25/90/PDF/thehabil.pdf
Publikováno v:
Logical Methods in Computer Science, Volume 11, Issue 3 (September 3, 2015) lmcs:1583
We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard moda
Externí odkaz:
http://arxiv.org/abs/1505.06896