Related papers: A Coinductive Version of Milner's Proof System for…
We extend to natural deduction the approach of Linear Nested Sequents and of 2-sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction -- only one…
The {\em spectrum} of a first-order logic sentence is the set of natural numbers that are cardinalities of its finite models. In this paper we show that when restricted to using only two variables, but allowing counting quantifiers, the…
Counterfactual reasoning is a foundational topic in both philosophical and logical studies \cite{Stalnaker1968-STAATO-5, Lewis1973-LEWC-2}. A pivotal component of counterfactual analysis is the concept of similarity between possible worlds…
Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have…
We provide a sound and complete proof system for an extension of Kleene's ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of…
In standard process algebra, parallel components do not share a common state and communicate through synchronisation. The advantage of this type of communication is that it facilitates compositional reasoning. For modelling and analysing…
We introduce and study single-conclusioned nested sequent calculi for a broad class of intuitionistic multi-modal logics known as "intuitionistic grammar logics (IGLs)." These logics serve as the intuitionistic counterparts of classical…
Autoformalization aims to produce formal statements that compile and faithfully preserve the intended meaning of informal mathematics. Yet standard single-output evaluation protocols collapse a many-to-many problem into a single-output…
Modal dependence logic (MDL) was introduced recently by V\"a\"an\"anen. It enhances the basic modal language by an operator =(). For propositional variables p_1,...,p_n the atomic formula =(p_1,...,p_(n-1),p_n) intuitively states that the…
There has been a significant interest in extending various modal logics with intersection, the most prominent examples being epistemic and doxastic logics with distributed knowledge. Completeness proofs for such logics tend to be…
We introduce a new two-sided type system for verifying the correctness and incorrectness of functional programs with atoms and pattern matching. A key idea in the work is that types should range over sets of normal forms, rather than sets…
We target the problem of provably computing the equivalence between two complex expression trees. To this end, we formalize the problem of equivalence between two such programs as finding a set of semantics-preserving rewrite rules from one…
For the general obstacle problem, we prove by direct methods an epiperimetric inequality at regular and singular points, thus answering a question of Weiss (Invent. Math., 138 (1999), 23--50). In particular at singular points we introduce a…
The unification algorithm has long been a target for program synthesis research, but a fully automatic derivation remains a research goal. In deductive program synthesis, computer programming is phrased as a task in theorem proving; a…
We investigate a coupled system of elliptic equations of Lane--Emden--Fowler type on a bounded domain $\Omega \subset \mathbb{R}^n$ ($n \geq 1$) with homogeneous Dirichlet boundary conditions. The system is characterized by sublinear…
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond…
Language models are increasingly being used in important decision pipelines, so ensuring the correctness of their outputs is crucial. Recent work has proposed evaluating the "factuality" of claims decomposed from a language model generation…
Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs. In this paper we give an alternative…
In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules.…
We introduce Probabilistic Regular Expressions (PRE), a probabilistic analogue of regular expressions denoting probabilistic languages in which every word is assigned a probability of being generated. We present and prove the completeness…