Related papers: Experiments with Choice in Dependently-Typed Highe…
Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder are just…
This work contributes to the domains of Boolean algebra and of Bayesian probability, by proposing an algebraic extension of Boolean algebras, which implements an operator for the Bayesian conditional inference and is closed under this…
Model checking for Halpern and Shoham's interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics). Here,…
In a previous paper, a tableau calculus has been presented, which constitute a decision procedure for hybrid logic with the converse and global modalities and a restricted use of the binder. This work extends such a calculus to multi-modal…
Realizability interprets propositions as specifications for computational entities in programming languages. Specifically, syntactic realizability is a powerful machinery that handles realizability as a syntactic translation of propositions…
This paper presents a simple decidable logic of functional dependence LFD, based on an extension of classical propositional logic with dependence atoms plus dependence quantifiers treated as modalities, within the setting of generalized…
The expression problem describes a fundamental tradeoff between two types of extensibility: extending a type with new operations, such as by pattern matching on an algebraic data type in functional programming, and extending a type with new…
Classical 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…
We study the problem of rewriting an ontology O1 expressed in a DL L1 into an ontology O2 in a Horn DL L2 such that O1 and O2 are equisatisfiable when extended with an arbitrary dataset. Ontologies that admit such rewritings are amenable to…
This paper proposes a connection method \`a la Bibel for an exception-tolerant family of description logics (DLs). As for the language, we assume the DL $\mathcal{ALCH}$ extended with two typicality operators: one on (complex) concepts and…
We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we…
A classical result in descriptive complexity theory states that Datalog expresses exactly the class of polynomially computable queries on ordered databases. In this paper we extend this result to the case of higher-order Datalog. In…
Many theories of semantic interpretation use lambda-term manipulation to compositionally compute the meaning of a sentence. These theories are usually implemented in a language such as Prolog that can simulate lambda-term operations with…
Higher-order logic programming is an interesting extension of traditional logic programming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order characteristics are indeed…
Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to…
We study how to infer new choices from prior choices using the framework of choice functions, a unifying mathematical framework for decision-making based on sets of preference orders. In particular, we define the natural (most conservative)…
Fiore and Hur recently introduced a conservative extension of universal algebra and equational logic from first to second order. Second-order universal algebra and second-order equational logic respectively provide a model theory and a…
We study two classes of extension problems, and their interconnections: (i) Extension of positive definite (p.d.) continuous functions defined on subsets in locally compact groups $G$; (ii) In case of Lie groups, representations of the…
The use of Extended Logics to replace ordinary second order definability in Kleene's {\em Ramified Analytical Hierarchy} is investigated. This mirrors a similar investigation of Kennedy, Magidor and V\"a\"an\"anen \cite{KeMaVa2016} where…
We define the notion of a model of higher-order modal logic in an arbitrary elementary topos $\mathcal{E}$. In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of propositions is not interpreted by the…