Related papers: Adelfa: A System for Reasoning about LF Specificat…
The work relates to the automatic generation of logical specifications, considered as sets of temporal logic formulas, extracted directly from developed software models. The extraction process is based on the assumption that the whole…
Declarative process specifications define the behavior of processes by means of rules based on Linear Temporal Logic on Finite Traces (LTLf). In a mining context, these specifications are inferred from, and checked on, multi-sets of runs…
The formal system lambda-delta is a typed lambda calculus that pursues the unification of terms, types, environments and contexts as the main goal. lambda-delta takes some features from the Automath-related lambda calculi and some from the…
The draft paper defines a system, which is capable of maintaining bases of test cases for logical specifications. The specifications, which are subject to this system are transformed from their original shape in first-order logic to…
Artificial intelligence systems have achieved remarkable capability in natural language processing, perception and decision-making tasks. However, their behaviour often remains opaque and difficult to verify, limiting their applicability in…
Verification is one of the central tasks in circuit and system design. While simulation and emulation are widely used, complete correctness can only be ensured based on formal proof techniques. But these approaches often have very high run…
We present a novel automata-based approach to address linear temporal logic modulo theory (LTL-MT) as a specification language for data words. LTL-MT extends LTL_f by replacing atomic propositions with quantifier-free multi-sorted…
Reasoning is essential for closed-domain QA systems in which procedural correctness and policy compliance are critical. While large language models (LLMs) have shown strong performance on many reasoning tasks, recent work reveals that their…
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the…
In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial…
The relationship between Lexical-Functional Grammar (LFG) functional structures (f-structures) for sentences and their semantic interpretations can be expressed directly in a fragment of linear logic in a way that explains correctly the…
Our research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and…
This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic,…
We introduce a new nameless representation of lambda terms inspired by ordered logic. At a lambda abstraction, number and relative position of all occurrences of the bound variable are stored, and application carries the additional…
Large Language Models (LLMs) have demonstrated remarkable efficiency in tackling various tasks based on human instructions, but studies reveal that they often struggle with tasks requiring reasoning, such as math or physics. This limitation…
The logic of definitions is a family of logics for encoding and reasoning about judgments, which are atomic predicates specified by inference rules. A definition associates an atomic predicate with a logical formula, which may itself depend…
Large language models (LLMs) are increasingly explored as general-purpose reasoners, particularly in agentic contexts. However, their outputs remain prone to mathematical and logical errors. This is especially challenging in open-ended…
In this work, we introduce DeepDFA, a novel approach to identifying Deterministic Finite Automata (DFAs) from traces, harnessing a differentiable yet discrete model. Inspired by both the probabilistic relaxation of DFAs and Recurrent Neural…
Formal theorem proving with TLA+ provides rigorous guarantees for system specifications, but constructing proofs requires substantial expertise and effort. While large language models have shown promise in automating proofs for tactic-based…
We present a unifying framework for type systems for process calculi. The core of the system provides an accurate correspondence between essentially functional processes and linear logic proofs; fragments of this system correspond to…