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.

Sample Sizes : None.

Authors: 2

Total Words: 0

Unqiue Words: 0

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.

Sample Sizes : None.

Authors: 4

Total Words: 0

Unqiue Words: 0

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.

arxiv_cslo:
A graph-based spatial temporal logic for knowledge representation and automated reasoning in cognitive robots https://t.co/LRNfS18s7A

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 0

Unqiue Words: 0

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.

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.

Sample Sizes : None.

Authors: 5

Total Words: 0

Unqiue Words: 0

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.

arxiv_cslo:
Modular coinduction up-to for higher-order languages via first-order transition systems https://t.co/tr2mrlUqg8

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 0

Unqiue Words: 0

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.

arxiv_cslo:
Semantics for first-order affine inductive data types via slice categories https://t.co/bwGl9ctUhx

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 0

Unqiue Words: 0

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.

arxiv_cslo:
Infinitary Action Logic with Exponentiation https://t.co/7QqQ8lXgOW

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 0

Unqiue Words: 0

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.

Sample Sizes : None.

Authors: 1

Total Words: 6656

Unqiue Words: 1658

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.

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.

Sample Sizes : None.

Authors: 4

Total Words: 0

Unqiue Words: 0

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.

arxiv_cslo:
Pumping lemmas for weighted automata https://t.co/HICtmU25wx

None.

None.

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

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible