Let \mathcal C be a class of finite and infinite graphs that is closed under induced subgraphs. the well-known Łoś-Tarski theorem from classical model theory implies that \mathcal C is definable in first-order logic (...
详细信息
We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC)---a system of higher-order logic modulo theories---and prove its soundness and refutational completeness w.r.t. both standa...
We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC)---a system of higher-order logic modulo theories---and prove its soundness and refutational completeness w.r.t. both standard and Henkin semantics. As corollaries, we obtain the compactness theorem and semi-decidability of HoCHC for semi-decidable background theories, and we prove that HoCHC satisfies a canonical model property. Moreover a variant of the well-known translation from higher-order to 1st-order logic is shown to be sound and complete for HoCHC in both semantics. We illustrate how to transfer decidability results for (fragments of) 1st-order logic modulo theories to our higher-order setting, using as example the Bernays-Schönfinkel-Ramsey fragment of HoCHC modulo a restricted form of Linear Integer Arithmetic.
We prove algorithmic undecidability of the (in)equational theory of residuated Kleene lattices (action lattices), thus solving a problem left open by D. Kozen, P. Jipsen, W. Buszkowski.
ISBN:
(纸本)9781728136080
We prove algorithmic undecidability of the (in)equational theory of residuated Kleene lattices (action lattices), thus solving a problem left open by D. Kozen, P. Jipsen, W. Buszkowski.
We 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 ...
详细信息
ISBN:
(纸本)9781728136080
We 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. We show that hypotheses defined by FOCN(P)-formulas over structures of polylogarithmic degree can be learned in sublinear time. Furthermore, we prove that for structures of unbounded degree there is no sublinear learning algorithm for first-order formulas.
In quantitative reasoning one compares objects by distances, instead of equivalence relations, so that one can measure how much they are similar, rather than just saying whether they are equivalent or not. In this pap...
详细信息
ISBN:
(纸本)9781450393515
In quantitative reasoning one compares objects by distances, instead of equivalence relations, so that one can measure how much they are similar, rather than just saying whether they are equivalent or not. In this paper we aim at providing a logical ground to quantitative reasoning with distances in Linear logic, using the categorical language of Lawvere’s doctrines. the key idea is to see distances as equality predicates in Linear logic. We use graded modalities to write a resource sensitive substitution rule for equality, which allows us to give it a quantitative meaning by distances. We introduce a deductive calculus for (Graded) Linear logic with quantitative equality and the notion of Lipschitz doctrine to give it a sound and complete categorical semantics. We also describe a universal construction of Lipschitz doctrines, which generates examples based for instance on metric spaces and quantitative realisability.
We introduce two extensions of the A -calculus with a probabilistic choice operator, A"ar and g'n, modeling respectively call -by -value and call-by-name probabilistic computation. We prove that both enjoys c...
详细信息
ISBN:
(纸本)9781728136080
We introduce two extensions of the A -calculus with a probabilistic choice operator, A"ar and g'n, modeling respectively call -by -value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. the common root of the two calculi is a further calculus based on Linear logic, A',D, which allows us to develop a unified, modular approach.
We give a geometry of interaction model for a typed gimel-calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Baye...
详细信息
ISBN:
(纸本)9781728136080
We give a geometry of interaction model for a typed gimel-calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. the model is based on the category of measurable spaces and partial measurable functions, and is proved adequate with respect to both a distribution-based and a sampling-based operational semantics.
We extend our recent template game model of multiplicative additive linear logic (MALL) with an exponential modality of linear logic (LL) derived from the standard categorical construction Sym of the free symmetric mo...
详细信息
ISBN:
(纸本)9781728136080
We extend our recent template game model of multiplicative additive linear logic (MALL) with an exponential modality of linear logic (LL) derived from the standard categorical construction Sym of the free symmetric monoidal category. We obtain in this way the first game semantics of differential linear logic (DiLL) in its classical form. the construction of the model relies on a careful and healthy comparison withthe model of generalised species designed ten years ago by Fiore, Gambino, Hyland and Winskel. Besides the resolution of an old open problem of game semantics, the study reveals an unexpected and promising convergence between linear logic and homotopy theory.
We propose a seamless integration of the block product operation to the recently developed algebraic framework for regular languages of countable words. A simple but subtle accompanying block product principle has bee...
详细信息
ISBN:
(纸本)9781728136080
We propose a seamless integration of the block product operation to the recently developed algebraic framework for regular languages of countable words. A simple but subtle accompanying block product principle has been established. Building on this, we generalize the well-known algebraic characterizations of first-order logic (resp. first-order logic with two variables) in terms of strongly (resp. weakly) iterated block products. We use this to arrive at a complete analogue of Schutzenberger-McNaughton-Papert theorem for countable words. We also explicate the role of block products for linear temporal logic by formulating a novel algebraic characterization of a natural fragment.
Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the gener...
Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open *** this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone μ-calculus, the variant of the polymodal μ-calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone μ-calculus.
暂无评论