total 11640took 0.10s

Reasoning in Highly Reactive EnvironmentsSep 18 2019The aim of my Ph.D. thesis concerns Reasoning in Highly Reactive Environments. As reasoning in highly reactive environments, we identify the setting in which a knowledge-based agent, with given goals, is deployed in an environment subject to repeated, ... More

Design of a Solver for Multi-Agent Epistemic PlanningSep 18 2019As the interest in Artificial Intelligence continues to grow it is becoming more and more important to investigate formalization and tools that allow us to exploit logic to reason about the world. In particular, given the increasing number of multi-agents ... More

Towards Ethical Machines Via Logic ProgrammingSep 18 2019Autonomous intelligent agents are playing increasingly important roles in our lives. They contain information about us and start to perform tasks on our behalves. Chatbots are an example of such agents that need to engage in a complex conversations with ... More

Extended Magic for Negation: Efficient Demand-Driven Evaluation of Stratified Datalog with Precise Complexity GuaranteesSep 18 2019Given a set of Datalog rules, facts, and a query, answers to the query can be inferred bottom-up starting from the facts or top-down starting from the query. For efficiency, top-down evaluation is extended with memoization of inferred facts, and bottom-up ... More

A Three-Valued Semantics for Typed Logic ProgrammingSep 18 2019Types in logic programming have focused on conservative approximations of program semantics by regular types, on one hand, and on type systems based on a prescriptive semantics defined for typed programs, on the other. In this paper, we define a new semantics ... More

Exploiting Partial Knowledge in Declarative Domain-Specific Heuristics for ASPSep 18 2019Domain-specific heuristics are an important technique for solving combinatorial problems efficiently. We propose a novel semantics for declarative specifications of domain-specific heuristics in Answer Set Programming (ASP). Decision procedures that are ... More

A descriptive Main Gap TheoremSep 17 2019Answering one of the main questions of [FHK14, Chapter 7], we show that there is a tight connection between the depth of a classifiable shallow theory $T$ and the Borel rank of the isomorphism relation $\cong^\kappa_T$ on its models of size $\kappa$, ... More

Axiomatizing logics of fuzzy preferences using graded modalitiesSep 17 2019The aim of this paper is to propose a many-valued modal framework to formalize reasoning with both graded preferences and propositions, in the style of van Benthem et al.'s classical modal logics for preferences. To do so, we start from Bou et al.'s minimal ... More

Simple Fixpoint Iteration To Solve Parity GamesSep 17 2019A naive way to solve the model-checking problem of the mu-calculus uses fixpoint iteration. Traditionally however mu-calculus model-checking is solved by a reduction in linear time to a parity game, which is then solved using one of the many algorithms ... More

Resource-Aware Automata and Games for Optimal SynthesisSep 17 2019We consider quantitative notions of parity automaton and parity game aimed at modelling resource-aware behaviour, and study (memory-full) strategies for exhibiting accepting runs that require a minimum amount of initial resources, respectively for winning ... More

Proceedings 35th International Conference on Logic Programming (Technical Communications)Sep 17 2019Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to: Foundations: ... More

Preservation of $γ$-spaces and covering properties of productsSep 17 2019We prove that the Hurewicz property is not preserved by finite products in the Miller model. This is a consequence of the fact that Miller forcing preserves ground model $\gamma$-spaces.

A Linear Exponential Comonad in s-finite Transition Kernels and Probabilistic Coherent SpacesSep 17 2019This paper concerns a stochastic construction of probabilistic coherent spaces by employing novel ingredients (i) linear exponential comonads arising properly in the measure-theory (ii) continuous orthogonality between measures and measurable functions. ... More

On correctness of an n queens programSep 16 2019Thom Fr\"uhwirth presented a short, elegant and efficient Prolog program for the n queens problem. However the program may be seen as rather tricky and one may be not convinced about its correctness. This paper explains the program in a declarative way, ... More

A Substructural Epistemic Resource Logic: Theory and Modelling ApplicationsSep 16 2019We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents' local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic combines Boolean ... More

RuDaS: Synthetic Datasets for Rule Learning and Evaluation ToolsSep 16 2019Logical rules are a popular knowledge representation language in many domains, representing background knowledge and encoding information that can be derived from given facts in a compact form. However, rule formulation is a complex process that requires ... More

Extending and Automating Basic Probability Theory with Propositional Computability LogicSep 16 2019Classical probability theory is formulated using sets. In this paper, we extend classical probability theory with propositional computability logic. Unlike other formalisms, computability logic is built on the notion of events/games, which is central ... More

Modal operators on rings of continuous functionsSep 15 2019The well-known dualities in modal logic establish dual equivalences between various categories of Kripke frames and modal algebras. Thomason duality provides a dual equivalence between the category KF of all Kripke frames and the category cmma of completely ... More

Psi-Calculi Revisited: Connectivity and CompositionalitySep 14 2019Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Mechanised proofs of standard algebraic and congruence properties of ... More

Propagation complete encodings of smooth DNNF theoriesSep 14 2019We investigate conjunctive normal form (CNF) encodings of a function represented with a smooth decomposable negation normal form (DNNF). Several encodings of DNNFs and decision diagrams were considered by (Abio et al. 2016). The authors differentiate ... More

Branch and Bound for Piecewise Linear Neural Network VerificationSep 14 2019The success of Deep Learning and its potential use in many safety-critical applications has motivated research on formal verification of Neural Network (NN) models. In this context, verification means verifying whether a NN model satisfies certain input-output ... More

Controlling a Random Population is EXPTIME-hardSep 13 2019Bertrand et al. [1] (LMCS 2019) describe two-player zero-sum games in which one player tries to achieve a reachability objective in $n$ games (on the same finite arena) simultaneously by broadcasting actions, and where the opponent has full control of ... More

Reasoning about call-by-value: a missing result in the history of Hoare's logicSep 13 2019We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism, and in which the correctness proofs are linear ... More

Ramsey Theory on Infinite Structures and the Method of Strong Coding TreesSep 12 2019This article discusses some recent trends in Ramsey theory on infinite structures. Trees and their Ramsey theory have been vital to these investigations. The main ideas behind the author's recent method of trees with coding nodes are presented, showing ... More

Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal VerificationSep 12 2019This volume contains the proceedings of the Tenth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2019). The symposium took place in Bordeaux, France, from the 2nd to the 3rd of September 2010. The GandALF symposium ... More

Detecting Architectural Erosion using Runtime VerificationSep 12 2019The architecture of a system captures important design decisions for the system. Over time, changes in a system's implementation may lead to violations of specific design decisions. This problem is common in industry and known as architectural erosion. ... More

Open Multiparty SessionsSep 12 2019Multiparty sessions are systems of concurrent processes, which allow several participants to communicate by sending and receiving messages. Their overall behaviour can be described by means of global types. Typable multiparty session enjoy lock-freedom. ... More

Examples, counterexamples, and structure in bounded width algebrasSep 12 2019We study bounded width algebras which are minimal in the sense that every proper reduct does not have bounded width. We show that minimal bounded width algebras can be arranged into a pseudovariety with one basic ternary operation. We classify minimal ... More

Topology is irrelevant (in a dichotomy conjecture for infinite domain constraint satisfaction problems)Sep 12 2019The tractability conjecture for finite domain Constraint Satisfaction Problems (CSPs) stated that such CSPs are solvable in polynomial time whenever there is no natural reduction, in some precise technical sense, from the 3-SAT problem; otherwise, they ... More

Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOLSep 12 2019We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or invariant sets for ... More

Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPsSep 12 2019The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes ... More

Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction GuaranteesSep 11 2019Reinforcement Learning (RL) has emerged as an efficient method of choice for solving complex sequential decision making problems in automatic control, computer science, economics, and biology. In this paper we present a model-free RL algorithm to synthesize ... More

Proceedings 12th Interaction and Concurrency ExperienceSep 11 2019This volume contains the proceedings of ICE'19, the 12th Interaction and Concurrency Experience, which was held in Copenhagen, Denmark on the 20th and 21st of June 2019, as a satellite event of DisCoTec'19. The ICE workshop series features a distinguishing ... More

Abstraction for Zooming-In to Unsolvability Reasons of Grid-Cell ProblemsSep 11 2019Humans are capable of abstracting away irrelevant details when studying problems. This is especially noticeable for problems over grid-cells, as humans are able to disregard certain parts of the grid and focus on the key elements important for the problem. ... More

Quasipolynomial Set-Based Symbolic Algorithms for Parity GamesSep 11 2019Solving parity games, which are equivalent to modal $\mu$-calculus model checking, is a central algorithmic problem in formal methods. Besides the standard computation model with the explicit representation of games, another important theoretical model ... More

Towards Assume-Guarantee Profiles for Autonomous VehiclesSep 11 2019Sep 12 2019Rules or specifications for autonomous vehicles are currently formulated on a case-by-case basis, and put together in a rather ad-hoc fashion. As a step towards eliminating this practice, we propose a systematic procedure for generating a set of supervisory ... More

Towards Assume-Guarantee Profiles for Autonomous VehiclesSep 11 2019Rules or specifications for autonomous vehicles are currently formulated on a case-by-case basis, and put together in a rather ad-hoc fashion. As a step towards eliminating this practice, we propose a systematic procedure for generating a set of supervisory ... More

Non-forking and preservation of NIP and dp-rankSep 10 2019We investigate the question of whether the restriction of a NIP type $p\in S(B)$ which does not fork over $A\subseteq B$ to $A$ is also NIP, and the analogous question for dp-rank. We show that if $B$ contains a Morley sequence $I$ generated by $p$ over ... More

Constant factor approximation of MAX CLIQUESep 10 2019MAX CLIQUE problem (MCP) is an NPO problem, which asks to find the largest complete sub-graph in a graph $G, G = (V, E)$ (directed or undirected). MCP is well known to be $NP-Hard$ to approximate in polynomial time with an approximation ratio of $1 + ... More

Constant factor approximation of MAX CLIQUESep 10 2019Sep 17 2019MAX CLIQUE problem (MCP) is an NPO problem, which asks to find the largest complete sub-graph in a graph $G, G = (V, E)$ (directed or undirected). MCP is well known to be $NP-Hard$ to approximate in polynomial time with an approximation ratio of $1 + ... More

Constant factor approximation of MAX CLIQUESep 10 2019Sep 12 2019MAX CLIQUE problem (MCP) is an NPO problem, which asks to find the largest complete sub-graph in a graph $G, G = (V, E)$ (directed or undirected). MCP is well known to be $NP-Hard$ to approximate in polynomial time with an approximation ratio of $1 + ... More

A Bayesian Approach to Direct and Inverse Abstract Argumentation ProblemsSep 10 2019This paper studies a fundamental mechanism of how to detect a conflict between arguments given sentiments regarding acceptability of the arguments. We introduce a concept of the inverse problem of the abstract argumentation to tackle the problem. Given ... More

Synthesis of Boolean Networks from Biological Dynamical Constraints using Answer-Set ProgrammingSep 10 2019Boolean networks model finite discrete dynamical systems with complex behaviours. The state of each component is determined by a Boolean function of the state of (a subset of) the components of the network. This paper addresses the synthesis of these ... More

On CDCL-based proof systems with the ordered decision strategySep 09 2019We prove that conflict-driven clause learning SAT-solvers with the ordered decision strategy and the DECISION learning scheme are equivalent to ordered resolution. We also prove that, by replacing this learning scheme with its opposite that stops after ... More

Learning Concepts Definable in First-Order Logic with CountingSep 09 2019We study classification problems over relational background structures for hypotheses that are defined using logics with counting. The aim of this paper is to find learning algorithms running in time sublinear in the size of the background structure. ... More

A Rewriting Logic Approach to Stochastic and Spatial Constraint System Specification and VerificationSep 09 2019This paper addresses the issue of specifying, simulating, and verifying reactive systems in rewriting logic. It presents an executable semantics for probabilistic, timed, and spatial concurrent constraint programming ---here called stochastic and spatial ... More

On the Strong Equivalences for LPMLN ProgramsSep 09 2019LPMLN is a powerful knowledge representation and reasoning tool that combines the non-monotonic reasoning ability of Answer Set Programming (ASP) and the probabilistic reasoning ability of Markov Logic Networks (MLN). In this paper, we study the strong ... More

CISE3: Verificação de aplicações com consistência fraca em Why3Sep 09 2019In this article we present a tool for the verification of programs built on top replicated databases. The tool evaluates a sequential specification and deduces which operations need to be synchronized for the program to function properly in a distributed ... More

Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata -- Technical ReportSep 09 2019I/O conformance testing theories (e.g., ioco) are concerned with formally defining when observable output behaviors of an implementation conform to those permitted by a specification. Thereupon, several real-time extensions of ioco, usually called tioco, ... More

Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata -- Technical ReportSep 09 2019Sep 10 2019I/O conformance testing theories (e.g., ioco) are concerned with formally defining when observable output behaviors of an implementation conform to those permitted by a specification. Thereupon, several real-time extensions of ioco, usually called tioco, ... More

The Cook-Reckhow definitionSep 09 2019The Cook-Reckhow 1979 paper defined the area of research we now call Proof Complexity. There were earlier papers which contributed to the subject as we understand it today, the most significant being Tseitin's 1968 paper, but none of them introduced general ... More

A dynamic epistemic logic analysis of the equality negation taskSep 07 2019In this paper we study the solvability of the equality negation task in a simple wait-free model where processes communicate by reading and writing shared variables or exchanging messages. In this task, two processes start with a private input value in ... More

Incompleteness Ex MachinaSep 06 2019In this essay we'll prove G\"odel's incompleteness theorems twice. First, we'll prove them the good old-fashioned way. Then we'll repeat the feat in the setting of computation. In the process we'll discover that G\"odel's work, rightly viewed, needs to ... More

The Complexity of Reachability in Affine Vector Addition Systems with StatesSep 05 2019We give a trichotomy on the complexity of integer reachability in vector addition systems with states extended with affine operations (affine VASS). Namely, we show that integer reachability in affine VASS is NP-complete for VASS with resets, PSPACE-complete ... More

Connected monads weakly preserve productsSep 05 2019If $F$ is a (not necessarily associative) monad on $Set$, then the natural transformation $F(A\times B)\to F(A)\times F(B)$ is surjective if and only if $F(\boldsymbol{1})=\boldsymbol{1}$. Specializing $F$ to $F_{\mathcal{V}}$, the free algebra functor ... More

Bisimulation maps in presheaf categoriesSep 04 2019The category of presheaves on a (small) category is a suitable semantic universe to study behaviour of various dynamical systems. In particular, presheaves can be used to record the executions of a system and their morphisms correspond to simulation maps ... More

Finitely Supported Sets Containing Infinite Uniformly Supported SubsetsSep 04 2019The theory of finitely supported algebraic structures represents a reformulation of Zermelo-Fraenkel set theory in which every construction is finitely supported according to the action of a group of permutations of some basic elements named atoms. In ... More

Probabilities in Session TypesSep 04 2019This paper deals with the probabilistic behaviours of distributed systems described by a process calculus considering both probabilistic internal choices and nondeterministic external choices. For this calculus we define and study a typing system which ... More

Proof-Based Synthesis of Sorting Algorithms Using Multisets in TheoremaSep 04 2019Using multisets, we develop novel techniques for mechanizing the proofs of the synthesis conjectures for list-sorting algorithms, and we demonstrate them in the Theorema system. We use the classical principle of extracting the algorithm as a set of rewrite ... More

(Co)inductive Proof Systems for Compositional Proofs in Reachability LogicSep 04 2019Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the ... More

Verifying the DPLL Algorithm in DafnySep 04 2019Modern high-performance SAT solvers quickly solve large satisfiability instances that occur in practice. If the instance is satisfiable, then the SAT solver can provide a witness which can be checked independently in the form of a satisfying truth assignment. ... More

Efficient elimination of Skolem functions in first-order logic without equalitySep 04 2019Sep 17 2019We prove that elimination of a single Skolem function in pure logic increases the length of cut-free proofs only linearly. The result is shown for a variant of sequent calculus with Henkin constants instead of free variables.

Efficient elimination of Skolem functions in first-order logic without equalitySep 04 2019We prove that elimination of a single Skolem function in pure logic increases the length of cut-free proofs only linearly. The result is shown for a variant of sequent calculus with Henkin constants instead of free variables.

Efficient elimination of Skolem functions in first-order logic without equalitySep 04 2019Sep 10 2019We prove that elimination of a single Skolem function in pure logic increases the length of cut-free proofs only linearly. The result is shown for a variant of sequent calculus with Henkin constants instead of free variables.

Complexity of controlled bad sequences over finite powersets of $\mathbb{N}^k$Sep 04 2019We provide lower and upper bounds for the length of controlled bad sequences over the majoring and the minoring ordering for finite powersets of $\mathbb{N}^k$. The results are obtained by bounding the length of such sequences by functions from the Cichon ... More

Complexity of controlled bad sequences over finite sets of $\mathbb{N}^k$Sep 04 2019Sep 13 2019We provide lower and upper bounds for the length of controlled bad sequences over the majoring and the minoring orderings for finite sets of $\mathbb{N}^k$. The results are obtained by bounding the length of such sequences by functions from the Cichon ... More

Complexity of controlled bad sequences over finite sets of $\mathbb{N}^k$Sep 04 2019Sep 08 2019We provide lower and upper bounds for the length of controlled bad sequences over the majoring and the minoring orderings for finite sets of $\mathbb{N}^k$. The results are obtained by bounding the length of such sequences by functions from the Cichon ... More

On the axiomatisability of the dual of compact ordered spacesSep 04 2019We provide a direct and elementary proof of the fact that the category of Nachbin's compact ordered spaces is dually equivalent to an Aleph_1-ary variety of algebras. Further, we show that Aleph_1 is a sharp bound: compact ordered spaces are not dually ... More

On the axiomatisability of the dual of compact ordered spacesSep 04 2019Sep 13 2019We provide a direct and elementary proof of the fact that the category of Nachbin's compact ordered spaces is dually equivalent to an Aleph_1-ary variety of algebras. Further, we show that Aleph_1 is a sharp bound: compact ordered spaces are not dually ... More

Classes of graphs with low complexity: the case of classes with bounded linear rankwidthSep 04 2019Classes with bounded rankwidth are MSO-transductions of trees and classes with bounded linear rankwidth are MSO-transductions of paths -- a result that shows a strong link between the properties of these graph classes considered from the point of view ... More

Value-centric Dynamic Partial Order ReductionSep 03 2019The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. ... More

Logic and the $2$-Simplicial TransformerSep 02 2019We introduce the $2$-simplicial Transformer, an extension of the Transformer which includes a form of higher-dimensional attention generalising the dot-product attention, and uses this attention to update entity representations with tensor products of ... More

DRAT and Propagation Redundancy Proofs Without New VariablesSep 02 2019We study the proof complexity of RAT proofs and related systems including BC, SPR and PR which use blocked clauses and (subset) propagation redundancy. These systems arise in satisfiability (SAT) solving, and allow inferences which preserve satisfiability ... More

Conditions for Unnecessary Logical Constraints in Kernel MachinesAug 31 2019A main property of support vector machines consists in the fact that only a small portion of the training data is significant to determine the maximum margin separating hyperplane in the feature space, the so called support vectors. In a similar way, ... More

Compositional specification in rewriting logicAug 30 2019Sep 04 2019Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose a complex system ... More

Compositional specification in rewriting logicAug 30 2019Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose a complex system ... More

The axiom of choice and model-theoretic structuresAug 30 2019We discuss the connections between the failure of the axiom of choice in set theory, and certain model-theoretic structures with enough symmetry.

Distality RankAug 29 2019We develop distality rank as a property of first-order theories and give examples for each rank $m$ such that $1\leq m \leq \omega$. For NIP theories, we show that distality rank is invariant under base change. We also define a generalization of type ... More

Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT LogicsAug 29 2019This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete ... More

The naturality of natural deduction (II). Some remarks on atomic polymorphismAug 29 2019In this paper (which is a prosecution of "The naturality of natural deduction", Studia Logica 2019) we investigate the exact relationship between the Russell-Prawitz translation of intuitionistic propositional logic into intuitionistc second-order propositional ... More

Factorization and Normalization, EssentiallyAug 29 2019Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or normalization theorems. In this paper we provide simple ... More

Cellular Monads from Positive GSOS SpecificationsAug 29 2019We give a leisurely introduction to our abstract framework for operational semantics based on cellular monads on transition categories. Furthermore, we relate it for the first time to an existing format, by showing that all Positive GSOS specifications ... More

PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order LogicAug 29 2019PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It includes a versatile formula macro system and supports the creation of documents that intersperse macro definitions, reasoner invocations and LaTeX-formatted ... More

Technical report of "The Knowledge Base Paradigm Applied to Delegation Revocation"Aug 29 2019In ownership-based access control frameworks with the possibility of delegating permissions and administrative rights, delegation chains will form. There are different ways to treat delegation chains when revoking rights, which give rise to different ... More

A universal characterization of standard Borel spacesAug 28 2019We prove that the category $\mathsf{SBor}$ of standard Borel spaces is the (bi-)initial object in the 2-category of countably complete Boolean (countably) extensive categories. This means that $\mathsf{SBor}$ is the universal category admitting some familiar ... More

A Type-Based HFL Model Checking AlgorithmAug 27 2019Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL ... More

Extending Description Logic EL++ with Linear Constraints on the Probability of AxiomsAug 27 2019One of the main reasons to employ a description logic such as EL or EL++ is the fact that it has efficient, polynomial-time algorithmic properties such as deciding consistency and inferring subsumption. However, simply by adding negation of concepts to ... More

Ordered Sets for Data AnalysisAug 27 2019This book dwells on mathematical and algorithmic issues of data analysis based on generality order of descriptions and respective precision. To speak of these topics correctly, we have to go some way getting acquainted with the important notions of relation ... More

Towards Constraint Logic Programming over Strings for Test Data GenerationAug 27 2019In order to properly test software, test data of a certain quality is needed. However, useful test data is often unavailable: Existing or hand-crafted data might not be diverse enough to enable desired test cases. Furthermore, using production data might ... More

Hilbert spaces and ${C}^\ast$-algebras are not finitely concreteAug 27 2019Sep 04 2019We show that no faithful functor from the category of Hilbert spaces with linear isometries into the category of sets preserves directed colimits. Thus Hilbert spaces cannot form an abstract elementary class, even up to change of language. We deduce an ... More

Hilbert spaces and ${C}^\ast$-algebras are not finitely concreteAug 27 2019We show that no faithful functor from the category of Hilbert spaces with linear isometries into the category of sets preserves directed colimits. Thus Hilbert spaces cannot form an abstract elementary class, even up to change of language. We deduce an ... More

Hilbert spaces and ${C}^\ast$-algebras are not finitely concreteAug 27 2019Sep 16 2019We show that no faithful functor from the category of Hilbert spaces with linear isometries into the category of sets preserves directed colimits. Thus Hilbert spaces cannot form an abstract elementary class, even up to change of language. We deduce an ... More

Model Theory of Proalgebraic GroupsAug 27 2019We lay the foundations for a model theoretic study of proalgebraic groups. Our axiomatization is based on the tannakian philosophy. Through a tensor analog of skeletal categories we are able to consider neutral tannakian categories with a fibre functor ... More

An Incompressibility Theorem for Automatic ComplexityAug 26 2019Shallit and Wang showed that the automatic complexity $A(x)\ge n/13$ for almost all $x\in\{0,1\}^n$. They also stated that Holger Petersen had informed them that the constant 13 can be reduced to 7. Here we show that it can be reduced to $2+\epsilon$ ... More

Introducing H, an institution-based formal specification and verification languageAug 26 2019This is a short survey on the development of the formal specification and verification language H with emphasis on the scientific part. H is a modern highly expressive language solidly based upon advanced mathematical theories such as the internalisation ... More

Dynamic Term-Modal Logic for Epistemic Social Network Dynamics (Extended Version)Aug 26 2019Logics for social networks have been studied in recent literature. This paper presents a framework based on *dynamic term-modal logic* (DTML), a quantified variant of dynamic epistemic logic (DEL). In contrast with DEL where it is commonly known to whom ... More

CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo TheoriesAug 26 2019We introduce an approach that aims to combine the usage of satisfiability modulo theories (SMT) solvers with the Combinatory Logic Synthesizer (CL)S framework. (CL)S is a tool for the automatic composition of software components from a user-specified ... More

Reconstructing veriT Proofs in Isabelle/HOLAug 26 2019Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified inside the proof ... More

EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)Aug 26 2019Proof assistants often call automated theorem provers to prove subgoals. However, each prover has its own proof calculus and the proof traces that it produces often lack many details to build a complete proof. Hence these traces are hard to check and ... More

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)Aug 26 2019This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver CVC4. While ... More