### Top 10 Arxiv Papers Today in Logic In Computer Science

##### #1. A symmetric protocol to establish service level agreements
###### J. F. Groote, T. A. C. Willemse
We present a symmetrical protocol to repeatedly negotiate a desired service level between two parties, where the service levels are taken from some totally ordered finite domain. The agreed service level is selected from the levels proposed by both parties and parties can only decrease the desired service level during a negotiation. The correctness of the protocol is stated using modal formulas and its behaviour is explained using behavioural reductions of the external behaviour modulo weak trace equivalence and divergence-preserving branching bisimulation. Our protocol originates from an industrial use case and it turned out be remarkably tricky to design correctly.
more | pdf | html
None.
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 2
Total Words: 0
Unqiue Words: 0

##### #2. Provenance for the Description Logic ELHr
###### Camille Bourgaux, Ana Ozaki, Rafael Peñaloza, Livia Predoiu
We address the problem of handling provenance information in ELHr ontologies. We consider a setting recently introduced for ontology-based data access, based on semirings and extending classical data provenance, in which ontology axioms are annotated with provenance tokens. A consequence inherits the provenance of the axioms involved in deriving it, yielding a provenance polynomial as an annotation. We analyse the semantics for the ELHr case and show that the presence of conjunctions poses various difficulties for handling provenance, some of which are mitigated by assuming multiplicative idempotency of the semiring. Under this assumption, we study three problems: ontology completion with provenance, computing the set of relevant axioms for a consequence, and query answering.
more | pdf | html
None.
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 4
Total Words: 0
Unqiue Words: 0

##### #3. A graph-based spatial temporal logic for knowledge representation and automated reasoning in cognitive robots
###### Zhiyu Liu, Meng Jiang, Hai Lin
A new graph-based spatial temporal logic is proposed for knowledge representation and automated reasoning in this paper. The proposed logic achieves a balance between expressiveness and tractability in applications such as cognitive robots. The satisfiability of the proposed logic is decidable. A Hilbert style axiomatization for the proposed graph-based spatial temporal logic is given where Modus ponens and IRR are the inference rules. It has been shown that the corresponding deduction system is sound and complete and can be implemented through constraint programming.
more | pdf | html
None.
###### Tweets
arxiv_cslo: A graph-based spatial temporal logic for knowledge representation and automated reasoning in cognitive robots https://t.co/LRNfS18s7A
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 3
Total Words: 0
Unqiue Words: 0

##### #4. Dynamic Epistemic Logic Games with Epistemic Temporal Goals
###### Bastien Maubert, Aniello Murano, Sophie Pinchinat, François Schwarzentruber, Silvia Stranieri
Dynamic Epistemic Logic (DEL) is a logical framework in which one can describe in great detail how actions are perceived by the agents, and how they affect the world. DEL games were recently introduced as a way to define classes of games with imperfect information where the actions available to the players are described very precisely. This framework makes it possible to define easily, for instance, classes of games where players can only use public actions or public announcements. These games have been studied for reachability objectives, where the aim is to reach a situation satisfying some epistemic property expressed in epistemic logic; several (un)decidability results have been established. In this work we show that the decidability results obtained for reachability objectives extend to a much more general class of winning conditions, namely those expressible in the epistemic temporal logic LTLK. To do so we establish that the infinite game structures generated by DEL public actions are regular, and we describe how to obtain...
more | pdf | html
None.
###### Tweets
SciFi: Dynamic Epistemic Logic Games with Epistemic Temporal Goals. https://t.co/fZW86T09Vk
arxiv_cslo: Dynamic Epistemic Logic Games with Epistemic Temporal Goals https://t.co/xQIrJOBfxP
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 5
Total Words: 0
Unqiue Words: 0

##### #5. Modular coinduction up-to for higher-order languages via first-order transition systems
###### Jean-Marie Madiot, Damien Pous, Davide Sangiorgi
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.
more | pdf | html
None.
###### Tweets
arxiv_cslo: Modular coinduction up-to for higher-order languages via first-order transition systems https://t.co/tr2mrlUqg8
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 3
Total Words: 0
Unqiue Words: 0

##### #6. Semantics for first-order affine inductive data types via slice categories
Affine type systems are substructural type systems where copying of information is restricted, but discarding of information is permissible at all types. Such type systems are well-suited for describing quantum programming languages, because copying of quantum information violates the laws of quantum mechanics. In this paper, we consider a first-order affine type system with inductive data types and present a novel categorical semantics for it. The most challenging aspect of this interpretation comes from the requirement to construct appropriate discarding maps for our data types which might be defined by mutual/nested recursion. We show how to achieve this for all types by taking models of a first-order linear type system whose atomic types are discardable and then presenting an additional affine interpretation of types within the slice category of the model with the tensor unit. We present some concrete categorical models for the language ranging from classical to quantum. Finally, we discuss potential ways of dualising and...
more | pdf | html
None.
###### Tweets
arxiv_cslo: Semantics for first-order affine inductive data types via slice categories https://t.co/bwGl9ctUhx
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 1
Total Words: 0
Unqiue Words: 0

##### #7. Infinitary Action Logic with Exponentiation
###### Stepan L. Kuznetsov, Stanislav O. Speranski
We introduce infinitary action logic with exponentiation---that is, the multiplicative-additive Lambek calculus extended with Kleene star and with a family of subexponential modalities, which allows some of the structural rules (contraction, weakening, permutation). The logic is presented in the form of an infinitary sequent calculus. We prove cut elimination and, in the case where at least one subexponential allows non-local contraction, establish exact complexity boundaries in two senses. First, we show that the derivability problem for this logic is $\Pi_1^1$-complete. Second, we show that the closure ordinal of its derivability operator is $\omega_1^{\mathrm{CK}}$.
more | pdf | html
None.
###### Tweets
arxiv_cslo: Infinitary Action Logic with Exponentiation https://t.co/7QqQ8lXgOW
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 2
Total Words: 0
Unqiue Words: 0

##### #8. Turing analogues of Gödel statements and computability of intelligence
###### Yasha Savelyev
We show that there is a mathematical obstruction to complete Turing computability of intelligence. This obstruction can be circumvented only if human reasoning is fundamentally unsound. The most compelling original argument for existence of such an obstruction was proposed by Penrose, however G\"odel, Turing and Lucas have also proposed such arguments. We first partially reformulate the argument of Penrose. In this formulation we argue that his argument works up to possibility of construction of a certain G\"odel statement. We then completely re-frame the argument in the language of Turing machines, and by partially defining our subject just enough, we show that a certain analogue of a G\"odel statement, or a G\"odel string as we call it in the language of Turing machines, can be readily constructed directly, without appeal to the G\"odel incompleteness theorem, and thus removing the final objection.
more | pdf | html
None.
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 1
Total Words: 6656
Unqiue Words: 1658

##### #9. Preservation of Equations by Monoidal Monads
###### Louis Parlant, Jurriaan Rot, Alexandra Silva, Bas Westerbaan
If a monad $T$ is monoidal, then operations on a set $X$ can be lifted canonically to operations on $TX$. In this paper we study structural properties under which $T$ preserves equations between those operations. It has already been shown that any monoidal monad preserves linear equations; affine monads preserve drop equations (where some variable appears only on one side, such as $x\cdot y = y$) and relevant monads preserve dup equations (where some variable is duplicated, such as $x \cdot x = x$). We start the paper by showing a converse: if the monad at hand preserves a drop equation, then it must be affine. From this, we show that the problem whether a given (drop) equation is preserved is undecidable. A converse for relevance turns out to be more subtle: preservation of certain dup equations implies a weaker notion which we call $n$-relevance. Finally, we identify the subclass of equations such that their preservation is equivalent to relevance.
more | pdf | html
None.
###### Tweets
mathCTbot: Louis Parlant, Jurriaan Rot, Alexandra Silva, Bas Westerbaan : Preservation of Equations by Monoidal Monads https://t.co/t0h9ZRPrm9 https://t.co/62gdm4SUKt
arxiv_cslo: Preservation of Equations by Monoidal Monads https://t.co/3vkrCJzkeH
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 4
Total Words: 0
Unqiue Words: 0

##### #10. Pumping lemmas for weighted automata
###### Agnishom Chattopadhyay, Filip Mazowiecki, Anca Muscholl, Cristian Riveros
We present pumping lemmas for five classes of functions definable by fragments of weighted automata over the min-plus semiring, the max-plus semiring and the semiring of natural numbers. As a corollary we show that the hierarchy of functions definable by unambiguous, finitely-ambiguous, polynomially-ambiguous weighted automata, and the full class of weighted automata is strict for the min-plus and max-plus semirings.
more | pdf | html
None.
###### Tweets
arxiv_cslo: Pumping lemmas for weighted automata https://t.co/HICtmU25wx
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 4
Total Words: 0
Unqiue Words: 0

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

Tracking 256,578 papers.

###### Search
Sort results based on if they are interesting or reproducible.
Interesting
Reproducible
Online
###### Stats
Tracking 256,578 papers.