We consider the problem of unification modulo an equational theory ACh, which
consists of a function h which is homomorphic over an associative-commutative
operator +. Unification modulo ACh is undecidable, so we define a bounded ACh
unification problem. In this bounded version of ACh unification we essentially
bound the number of times h can be recursively applied to a term, and only
allow solutions that satisfy this bound. There is no bound on the number of
occurrences of h in a term, and the + symbol can be applied an unlimited number
of times. We give inference rules for solving bounded ACh unification, and we
prove that the rules are sound, complete and terminating. We have implemented
the algorithm in Maude and give experimental results. We argue that this
algorithm is useful in cryptographic protocol analysis.

more |
pdf
| html
None.

ComputerPapers:
Bounded ACh Unification. https://t.co/L65Gx8F3BT

arxiv_cslo:
Bounded ACh Unification https://t.co/8HQAGmebZD

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 10664

Unqiue Words: 1608

This paper presents a study of causality in a reversible, concurrent setting.
There exist various notions of causality in pi-calculus, which differ in the
treatment of parallel extrusions of the same name. In this paper we present a
uniform framework for reversible pi-calculi that is parametric with respect to
a data structure that stores information about an extrusion of a name.
Different data structures yield different approaches to the parallel extrusion
problem. We map three well-known causal semantics into our framework. We show
that the (parametric) reversibility induced by our framework is causally-
consistent and prove a causal correspondence between an appropriate instance of
the framework and Boreale and Sangiorgi's causal semantics.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 19173

Unqiue Words: 2744

In Reasoning about Action and Planning, one synthesizes the agent plan by
taking advantage of the assumption on how the environment works (that is, one
exploits the environment's effects, its fairness, its trajectory constraints).
In this paper we study this form of synthesis in detail. We consider
assumptions as constraints on the possible strategies that the environment can
have in order to respond to the agent's actions. Such constraints may be given
in the form of a planning domain (or action theory), as linear-time formulas
over infinite or finite runs, or as a combination of the two (e.g., FOND under
fairness). We argue though that not all assumption specifications are
meaningful: they need to be consistent, which means that there must exist an
environment strategy fulfilling the assumption in spite of the agent actions.
For such assumptions, we study how to do synthesis/planning for agent goals,
ranging from a classical reachability to goal on traces specified in LTL and
LTLf/LDLf, characterizing the problem both...

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 9403

Unqiue Words: 2026

Leveraging topos theory a semantics can be given to sequential circuits where
time-sensitive gates, such as unit delay, are treated uniformly with
combinational gates. Both kinds of gates are functions in a particular topos:
the topos of presheaves over the natural ordering of $\mathbb{N}$. This is used
to show that sequential circuits validate the equational theory of traced
categories.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 5667

Unqiue Words: 1696

In recent years, expansion-based techniques have been shown to be very
powerful in theory and practice for solving quantified Boolean formulas (QBF),
the extension of propositional formulas with existential and universal
quantifiers over Boolean variables. Such approaches partially expand one type
of variable (either existential or universal) and pass the obtained formula to
a SAT solver for deciding the QBF. State-of-the-art expansion-based solvers
process the given formula quantifier-block wise and recursively apply expansion
until a solution is found.
In this paper, we present a novel algorithm for expansion-based QBF solving
that deals with the whole quantifier prefix at once. Hence recursive
applications of the expansion principle are avoided. Experiments indicate that
the performance of our simple approach is comparable with the state of the art
of QBF solving, especially in combination with other solving techniques.

more |
pdf
| html
None.

ComputerPapers:
Expansion-Based QBF Solving Without Recursion. https://t.co/rLAF2C4OQ6

None.

None.

Sample Sizes : None.

Authors: 6

Total Words: 9458

Unqiue Words: 2277

Population protocols (Angluin et al., PODC, 2004) are a formal model of
sensor networks consisting of identical mobile devices. Two devices can
interact and thereby change their states. Computations are infinite sequences
of interactions satisfying a strong fairness constraint.
A population protocol is well-specified if for every initial configuration
$C$ of devices, and every computation starting at $C$, all devices eventually
agree on a consensus value depending only on $C$. If a protocol is
well-specified, then it is said to compute the predicate that assigns to each
initial configuration its consensus value.
In a previous paper we have shown that the problem whether a given protocol
is well-specified and the problem whether it computes a given predicate are
decidable. However, in the same paper we prove that both problems are at least
as hard as the reachability problem for Petri nets. Since all known algorithms
for Petri net reachability have non-primitive recursive complexity, in this
paper we restrict attention to...

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 12490

Unqiue Words: 2257

We study the logical complexity of proofs in cyclic arithmetic
($\mathsf{CA}$), as introduced in Simpson '17, in terms of quantifier
alternations of formulae occurring. Writing $C\Sigma_n$ for (the logical
consequences of) cyclic proofs containing only $\Sigma_n$ formulae, our main
result is that $I\Sigma_{n+1}$ and $C\Sigma_n$ prove the same $\Pi_{n+1}$
theorems, for all $n\geq 0$. Furthermore, due to the 'uniformity' of our
method, we also show that $\mathsf{CA}$ and Peano Arithmetic ($\mathsf{PA}$)
proofs of the same theorem differ only exponentially in size.
The inclusion $I\Sigma_{n+1} \subseteq C\Sigma_n$ is obtained by proof
theoretic techniques, relying on normal forms and structural manipulations of
$\mathsf{PA}$ proofs. It improves upon the natural result that $I\Sigma_n$ is
contained in $C\Sigma_n$. The converse inclusion, $C\Sigma_n \subseteq
I\Sigma_{n+1}$, is obtained by calibrating the approach of Simpson '17 with
recent results on the reverse mathematics of B\"uchi's theorem in
Ko{\l}odziejczyk, Michalewski,...

more |
pdf
| html
None.

ComputerPapers:
On the logical complexity of cyclic arithmetic. https://t.co/WutTvE5LZi

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 15872

Unqiue Words: 3338

In computer science, category theory remains a contentious issue, with
enthusiastic fans and a skeptical majority. Categories were introduced by
Samuel Eilenberg and Saunders Mac Lane as an auxiliary notion in their general
theory of natural equivalences. Here we argue that something like categories is
needed on a more basic level. As you work with operations on structures, it may
be necessary to coherently manipulate isomorphism (or more generally
homomorphism) witnesses for various properties of these operations, e.g.\
associativity, commutativity and distributivity. A working mathematician, to
use Mac Lane's term, is well advised to be aware of the coherent
witness-manipulation problem and to know that category theory is an appropriate
framework to address the problem. Of course, the working mathematician in
question may be a computer scientist or physicist.

more |
pdf
| html
None.

paper3510mm:
Who needs category theory? / Andreas Blass, Yuri Gurevich / (Submitted on 30 Jul 2018)
https://t.co/k4ZsF0oQzC
目を通したけどよくわかんなかった

philipthrift:
"We didn’t want to rule out possible alternatives."
https://t.co/e35CdpPSzm

paper3510mm:
RT @QuantumToy: Who needs category theory?
https://t.co/pWMOOU8WAo
In computer science, category theory remains a contentious issue, with e…

AIcia_Solid:
RT @QuantumToy: Who needs category theory?
https://t.co/pWMOOU8WAo
In computer science, category theory remains a contentious issue, with e…

koburouze845:
RT @QuantumToy: Who needs category theory?
https://t.co/pWMOOU8WAo
In computer science, category theory remains a contentious issue, with e…

mathcurve:
RT @arxiv_cslo: Who needs category theory? https://t.co/ECCotmOhlJ

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 2132

Unqiue Words: 841

This work presents a compositional approach for schedulability analysis of
Distributed Integrated Modular Avionics (DIMA) systems that consist of
spatially distributed ARINC-653 modules connected by a unified AFDX network. We
model a DIMA system as a set of stopwatch automata in UPPAAL to verify its
schedulability by model checking. However, direct model checking is infeasible
due to the large state space. Therefore, we introduce the compositional
analysis that checks each partition including its communication environment
individually. Based on a notion of message interfaces, a number of message
sender automata are built to model the environment for a partition. We define a
timed selection simulation relation, which supports the construction of
composite message interfaces. By using assume-guarantee reasoning, we ensure
that each task meets the deadline and that communication constraints are also
fulfilled globally. The approach is applied to the analysis of a concrete DIMA
system.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 6597

Unqiue Words: 1869

Intelligent technologies, in particular systems to promote health and
well-being, are inherently centered around the human being, and they need to
interrelate with human activities at their core. While social sciences provide
angles to study such activities, e.g., within the framework of
cultural-historical activity theory, there is no formal approach to give an
account of complex human activities from a Knowledge Representation and
Reasoning (KR) perspective. Our goal is to develop a logic-based framework to
specify complex activities that is directly informed by activity theory. There,
complex activity refers to the process that mediates the relation between a
subject and some motivating object which in turn generates a hierarchy of goals
that direct actions. We introduce a new temporal logic to formalise key
concepts from activity theory and study various inference problems in our
framework. We furthermore discuss how to use Answer-Set Programming as a KR
shell for activity reasoning that allows to solve various reasoning tasks...

more |
pdf
| html
None.

ComputerPapers:
A Knowledge Representation Perspective on Activity Theory. https://t.co/gh8GklZmpo

arxiv_cslo:
A Knowledge Representation Perspective on Activity Theory https://t.co/07rOGY8I2X

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 10337

Unqiue Words: 2635

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 72,995 papers.*

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible