SMT solvers increasingly produce proof certificates to meet the trust requirements of safety-critical applications. However, eagerly justifying learned theory lemmas during solving constitutes a major performance bottleneck. Recent work mitigates this cost by emitting proof skeletons that record only SAT reasoning and unannotated theory lemmas, though existing approaches depend on new proof formats and specialized theory-specific tooling. We present a general approach that restricts SMT proof skeletons to core SMT reasoning: preprocessing, clausification, and unannotated theory lemmas. We develop external tools for SAT reasoning and proof trimming that reduce the number of theory lemmas requiring justification. An experimental evaluation using the SMT solver cvc5 on SMT-LIB benchmarks across the UF, LIA and LRA theories, with and without quantifiers, demonstrates faster solving and competitive checking performance compared to eager proof production, particularly on quantifier-free problems.
Prolog is traditionally thought of as an untyped logic programming language, although there are queries that result in a type error. Several attempts of statically introducing a type discipline in Prolog have been made but they have not been widely adopted. We use Maude to implement a typed unification algorithm and use it as the basis for an interpreter for Prolog called MaudeTypedLog. This interpreter follows the Typed SLD-resolution operational semantics for logic programming, that makes it possible to detect type errors in both programs and queries dynamically.
In this paper, we present a dynamic logic with parallel operators for the formal verification of authenticity and safety properties of cryptographic protocols. The logic incorporates communication actions and is specifically designed to reason about protocol executions in adversarial environments. We extend an existing dynamic logic with parallel operators by introducing concepts derived from the Dolev-Yao intruder model. As the underlying logic is completely axiomatizable, we obtain a complete axiomatization for the extended system. Furthermore, we develop a tableau calculus for the proposed logic and prove its termination, soundness, and completeness.
Robust classification is commonly understood as the stability of a classifier under small perturbations (often adversarial) of input data. In this paper, we propose a logical framework for robust classification grounded in topological semantics for modal logic. Evaluation points are feature vectors representing machine-readable objects, and formulas express explicit classifications. Robustness is interpreted geometrically as local truth persistence: a classification is robust at a point if it holds throughout some non-empty open neighbourhood of that point. Building on this perspective, we introduce a logical language with a robustness modality interpreted over S4 topological spaces, together with a robustness-sensitive conditional connective. This conditional connective captures global inclusion relations between robust regions and other properties of the classifier: it holds at a point when the neighbourhood witnessing the robustness of one formula is contained in the truth set of another. In this way, robust classifications can be systematically linked to classification conditions. We provide a sound and complete axiomatisation of the resulting logic. Finally, we introduce Minimal Robust Models, a constructive method for generating models from specified robustness constraints, which yields formal tools for analysing, explaining, and structuring robust classification behaviour.
The General Data Protection Regulation (GDPR) establishes purpose limitation as a fundamental constraint on personal data processing: personal data must be collected, stored, and processed strictly in accordance with explicitly specified purposes. Therefore, systems are required not only to declare the purposes under which personal data are processed, but also to ensure that their runtime behaviour remains aligned with the declared purposes. Yet, in mainstream software engineering practice, purposes are often treated as informal declarations, largely disconnected from system behaviour and, therefore, not amenable to rigorous reasoning about purpose compliance. This gap becomes particularly problematic in distributed systems, where personal data may flow across multiple entities and evolve through complex communication patterns. To address this challenge, recent works propose a more elaborate treatment of purposes based on structured, action-oriented representations of the data-processing interactions involved in their fulfilment. Building on these insights, we introduce a formal, purpose-aware framework grounded in multiparty session types in which purposes are modelled as structured interaction protocols among system entities. Within our framework, system implementations are specified using a process calculus that captures the semantics of distributed interactions and features private data as a first-class entity. Furthermore, we define a type system that verifies compliance between declared purposes and system models, and we establish subject reduction and purpose fidelity results, thereby ensuring that well-typed systems do not deviate from their specified purposes during execution. We demonstrate our approach through a case study involving a healthcare system. Ultimately, our objective is to evolve this formal framework into a software-engineering-oriented approach that unifies purpose modelling and compliance verification within a lifecycle-driven methodology, thus enabling a practically applicable privacy-by-design process.
Term expansion was originally introduced in 2004 as a way to relate terms typed in an intersection type system with linear terms. Recently, new applications of term expansion include the relation of lambda-terms with terms typed in other substructural type systems, such as the relevant and the ordered type systems, and the use of quantitative types to relate the strongly normalising lambda-terms with weak linear terms that share the same normal form. Here we define a new term expansion for a calculus with explicit substitutions, using it to relate a lambda-calculus with explicit substitutions to Boudol's resource aware lambda-calculus with multiplicities, where function arguments have a possibly limited availability.
We propose a logical formalisation of computational errors in reactive, nondeterministic systems. To this aim, we introduce a new three-valued symmetric nondeterministic disjunction, designed to provide a faithful logical representation of the nondeterministic choice arising in concurrent computations. The connective is defined within the framework of nondeterministic matrices (Nmatrices) and derives from a minimal combination of Kleene's tolerant semantics and Bochvar's symmetric error persistence, thereby eliminating the residual asymmetry induced by sequential evaluation strategies such as McCarthy's logic. The resulting semantics admits genuinely nondeterministic outcomes in mixed cases involving errors, while preserving commutativity and operational symmetry.
In this paper we continue assessing the feasibility of the approach to the mechanization of type theory by using classical syntax and Stoughton's multiple substitutions and report some substantial progress. We present formal proofs of confluence for beta-reduction and by using Takahashi's revision of Tait and Martin-Löf's proof, subject reduction for the entire family of the Pure Type Systems and consistency for some impredicative subclass, assuming normalization. As to the proof of confluence, we also develop a theory of alpha-commutative relations which, in our view, entails a clearer presentation and treatment of the problem than in similar developments. Finally, we assess general merits and drawbacks of the approach. The whole development has been machine-checked using Agda.
In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), obtained via horizontal compression of Natural Deduction proofs in purely implicational minimal logic, as Boolean circuits. These DLDS compress Natural Deduction tree-like proofs into directed acyclic graphs, preserving logical correctness while reducing redundancy. We formally define the circuit construction process and establish its pointwise correctness, showing that, for any fixed path assignment, the resulting Boolean circuit agrees with the intended dependency-propagation semantics. A Lean formalization establishes machine-checked guarantees for the circuit evaluator and includes a restricted bridge for the uncompressed simple-tree fragment, connecting valid DLDS instances in that fragment to genuine circuit acceptance of their extracted paths under the route and discharge conditions formalized in Lean. This approach opens new perspectives for automated theorem proving and formal certification.
Path Predicate Modal Logic (PPML) is a generalization of Basic Modal Logic, where atoms are relational predicates instead of propositional symbols. The study of PPML is motivated as a way to abstractly investigate data-aware formalisms, such as XPath or DataGL. In this paper, we investigate some basic model theoretical aspects of PPML to better characterize its expressive power. More concretely, we investigate different ways of defining Hennessy-Milner classes, and a van Benthem characterization theorem. In doing so, we discuss the main challenges of dealing with the novel features of PPML, and what are the similarities with the standard approaches.
We introduce a typing system that is particularly well suited for typing the linear lambda-calculus in de Bruijn notation. This typing discipline, which is reminiscent of Hodas' and Miller's model of resource consumption, guarantees that any well-typed term is linear without the need for an occurrence check. We then establish the subject reduction property.
This paper establishes the cut-elimination theorem for intuitionistic propositional multiplicative-additive linear logic with the least and greatest fixpoints (μIMALL) by means of its phase semantics. A classical first-order multiplicative-additive linear logic system with the least and greatest fixpoints was introduced by Baelde and Miller (2007). Its intuitionistic fragment was discussed in Baelde (2012), but the cut-elimination theorem for this fragment has not yet been proved. We introduce a propositional fragment of this system, μIMALL, and establish the cut-elimination theorem. To prove the theorem, we define phase semantics for μIMALL and show the following two statements: (1) Soundness: if a formula is provable in μIMALL, then it is true in all phase models, and (2) Cut-free Completeness: if a formula is true in all phase models, then it is provable in μIMALL without Cut. Okada (1999, 2002) employed a phase semantic method to prove the cut-elimination theorems for classical and intuitionistic linear logic systems. De et al. (2022) applied this method to a propositional fragment of classical propositional multiplicative-additive linear logic with the least and greatest fixpoints. We refine and apply their arguments to prove the cut-elimination theorem for μIMALL.
