Top 10 Arxiv Papers Today in Logic In Computer Science


0.0 Mikeys
#1. Bounded ACh Unification
Ajay Kumar Eeralla, Christopher Lynch
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
Figures
None.
Tweets
ComputerPapers: Bounded ACh Unification. https://t.co/L65Gx8F3BT
arxiv_cslo: Bounded ACh Unification https://t.co/8HQAGmebZD
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 10664
Unqiue Words: 1608

0.0 Mikeys
#2. A Parametric Framework for Reversible $π$-Calculi
Doriana Medic, Claudio Antares Mezzina, Iain Phillips, Nobuko Yoshida
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 19173
Unqiue Words: 2744

0.0 Mikeys
#3. Planning and Synthesis Under Assumptions
Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Sasha Rubin
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 9403
Unqiue Words: 2026

0.0 Mikeys
#4. Circuits via topoi
Arnaud Spiwack
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 5667
Unqiue Words: 1696

0.0 Mikeys
#5. Expansion-Based QBF Solving Without Recursion
Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, Martina Seidl
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
Figures
None.
Tweets
ComputerPapers: Expansion-Based QBF Solving Without Recursion. https://t.co/rLAF2C4OQ6
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 6
Total Words: 9458
Unqiue Words: 2277

0.0 Mikeys
#6. Verification of Immediate Observation Population Protocols
Javier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 12490
Unqiue Words: 2257

0.0 Mikeys
#7. On the logical complexity of cyclic arithmetic
Anupam Das
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
Figures
None.
Tweets
ComputerPapers: On the logical complexity of cyclic arithmetic. https://t.co/WutTvE5LZi
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 15872
Unqiue Words: 3338

0.0 Mikeys
#8. Who needs category theory?
Andreas Blass, Yuri Gurevich
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
Figures
None.
Tweets
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
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 2132
Unqiue Words: 841

0.0 Mikeys
#9. A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems
Pujie Han, Zhengjun Zhai, Brian Nielsen, Ulrik Nyman
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 6597
Unqiue Words: 1869

0.0 Mikeys
#10. A Knowledge Representation Perspective on Activity Theory
Johannes Oetsch, Juan-Carlos Nieves
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
Figures
None.
Tweets
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
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 10337
Unqiue Words: 2635

About

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.

Search
Sort results based on if they are interesting or reproducible.
Interesting
Reproducible
Categories
All
Astrophysics
Cosmology and Nongalactic Astrophysics
Earth and Planetary Astrophysics
Astrophysics of Galaxies
High Energy Astrophysical Phenomena
Instrumentation and Methods for Astrophysics
Solar and Stellar Astrophysics
Condensed Matter
Disordered Systems and Neural Networks
Mesoscale and Nanoscale Physics
Materials Science
Other Condensed Matter
Quantum Gases
Soft Condensed Matter
Statistical Mechanics
Strongly Correlated Electrons
Superconductivity
Computer Science
Artificial Intelligence
Hardware Architecture
Computational Complexity
Computational Engineering, Finance, and Science
Computational Geometry
Computation and Language
Cryptography and Security
Computer Vision and Pattern Recognition
Computers and Society
Databases
Distributed, Parallel, and Cluster Computing
Digital Libraries
Discrete Mathematics
Data Structures and Algorithms
Emerging Technologies
Formal Languages and Automata Theory
General Literature
Graphics
Computer Science and Game Theory
Human-Computer Interaction
Information Retrieval
Information Theory
Machine Learning
Logic in Computer Science
Multiagent Systems
Multimedia
Mathematical Software
Numerical Analysis
Neural and Evolutionary Computing
Networking and Internet Architecture
Other Computer Science
Operating Systems
Performance
Programming Languages
Robotics
Symbolic Computation
Sound
Software Engineering
Social and Information Networks
Systems and Control
Economics
Econometrics
General Economics
Theoretical Economics
Electrical Engineering and Systems Science
Audio and Speech Processing
Image and Video Processing
Signal Processing
General Relativity and Quantum Cosmology
General Relativity and Quantum Cosmology
High Energy Physics - Experiment
High Energy Physics - Experiment
High Energy Physics - Lattice
High Energy Physics - Lattice
High Energy Physics - Phenomenology
High Energy Physics - Phenomenology
High Energy Physics - Theory
High Energy Physics - Theory
Mathematics
Commutative Algebra
Algebraic Geometry
Analysis of PDEs
Algebraic Topology
Classical Analysis and ODEs
Combinatorics
Category Theory
Complex Variables
Differential Geometry
Dynamical Systems
Functional Analysis
General Mathematics
General Topology
Group Theory
Geometric Topology
History and Overview
Information Theory
K-Theory and Homology
Logic
Metric Geometry
Mathematical Physics
Numerical Analysis
Number Theory
Operator Algebras
Optimization and Control
Probability
Quantum Algebra
Rings and Algebras
Representation Theory
Symplectic Geometry
Spectral Theory
Statistics Theory
Mathematical Physics
Mathematical Physics
Nonlinear Sciences
Adaptation and Self-Organizing Systems
Chaotic Dynamics
Cellular Automata and Lattice Gases
Pattern Formation and Solitons
Exactly Solvable and Integrable Systems
Nuclear Experiment
Nuclear Experiment
Nuclear Theory
Nuclear Theory
Physics
Accelerator Physics
Atmospheric and Oceanic Physics
Applied Physics
Atomic and Molecular Clusters
Atomic Physics
Biological Physics
Chemical Physics
Classical Physics
Computational Physics
Data Analysis, Statistics and Probability
Physics Education
Fluid Dynamics
General Physics
Geophysics
History and Philosophy of Physics
Instrumentation and Detectors
Medical Physics
Optics
Plasma Physics
Popular Physics
Physics and Society
Space Physics
Quantitative Biology
Biomolecules
Cell Behavior
Genomics
Molecular Networks
Neurons and Cognition
Other Quantitative Biology
Populations and Evolution
Quantitative Methods
Subcellular Processes
Tissues and Organs
Quantitative Finance
Computational Finance
Economics
General Finance
Mathematical Finance
Portfolio Management
Pricing of Securities
Risk Management
Statistical Finance
Trading and Market Microstructure
Quantum Physics
Quantum Physics
Statistics
Applications
Computation
Methodology
Machine Learning
Other Statistics
Statistics Theory
Feedback
Online
Stats
Tracking 72,995 papers.