To cater to the needs of (Zero Knowledge) proofs for (mathematical) proofs, we describe a method to transform formal sentences in 2 x 2 - matrices over multivariate polynomials with integer coefficients, such that usual proof-steps like modus-ponens or the substitution are easy to compute from the matrices corresponding to the terms or formulas used as arguments. By evaluating the polynomial variables in random elements of a suitably chosen finite field, the proof is replaced by a numeric sequence. Only the values corresponding to the axioms have to be computed from scratch. The values corresponding to derived formulas are computed from the values corresponding to their ancestors by applying the homomorphic properties. On such sequences, various Zero Knowledge methods can be applied.
NuITP is an inductive theorem prover that combines advanced symbolic techniques such as narrowing, equality predicates, variant unification, variant satisfiability, order-sorted congruence closure, ordered rewriting, and strategy-based rewriting (all applied modulo axioms) to verify equational programs with expressive features such as sorts and subsorts, conditional equations and rewriting modulo axioms in Maude and in other equational languages. This paper presents the tool, explains its inference rules, and illustrates their use in proving several examples with substantial levels of automated proof simplification based on symbolic techniques.
Constraint solving modulo equational theories plays a central role in symbolic computation, logic programming, and knowledge representation. In this paper, we extend classical constraint solving techniques by incorporating fuzzy similarity and proximity relations into constraint solving with unordered symbols. Our contributions include two constraint solving algorithms: one for similarity-based constraint solving, allowing mismatches between function symbol names, and another for proximity-based constraint solving, which also supports mismatches in arity. Both algorithms are supported by formal termination, soundness, and completeness proofs, and have been implemented in a user-friendly, web-based prototype. We analyze their computational complexity and discuss how these methods enhance expressiveness and enable approximate reasoning in contexts where strict syntactic matching is insufficient.
The concept of a context—a term with a hole—is fundamental to operational semantics and term rewriting, yet it is typically treated as a meta-theoretical artifact defined via grammars outside the logic. In this paper, we propose a rigorous theory of contexts reified as first-class objects within Matching Logic. We introduce a specific binder, the γ-abstraction, to represent holes, and define an axiomatic “plugging” operation. We prove that this logical plugging is semantically equivalent to capture-avoiding substitution. We further generalize this theory to handle multi-hole contexts through recursive sorts and currying, and introduce a composition operator for nested contexts. We demonstrate the theoretical and practical power of this framework through examples showing how to bridge high-level definitions of programming languages with their logical denotations.
Python’s typing system has evolved pragmatically into a powerful but theoretically fragmented system, with scattered specifications. This paper proposes a formalization to address this fragmentation. The central contribution is a formal foundation that uses existential types to elegantly describe Python’s type system. This work aims to serve as a fundamental first step towards the future development of type inference tools.
In this work, we propose a many-sorted hybrid modal logic framework for specification and verification of a neural network training process, using the established correspondence between multi-layer perceptrons and Łukasiewicz logic with rational coefficients. In our system, the operations of the training procedure are modal operators and the entire training dynamics is formalized as a sequence of logical deductions. Furthermore, we provide a implementation of our logic in the Lean proof assistant.
Unification is one of the fundamental operations in automated first-order reasoning and is used intensively in fields such as theorem proving and logic programming. Since Robinson’s pioneering proposal, several efficient algorithms based on sophisticated data structures have been developed, and some approaches to its parallelization have been analyzed.Recent advances in hardware, particularly the rise of Graphical Processing Units (GPUs), give us the opportunity to work with large volumes of data in parallel. The use of GPUs is becoming increasingly common in applications beyond computer graphics, thanks to their massive parallelism, high memory bandwidth, and throughput-oriented architecture. However, these advantages are best leveraged when working with data structures that exhibit high regularity, such as dense arrays or matrices. Unfortunately, inductively defined expressions, commonly used in unification, typically exhibit irregular and sparse structures, making them unsuitable for direct GPU acceleration.In this work, we present a new approach to efficiently unify large batches of terms by introducing a novel matrix-based representation that avoids the irregularities inherent in traditional approaches. We have implemented a C-based prototype that achieves competitive performance compared to a Prolog baseline, while also revealing how structural characteristics of the representation influence efficiency. This prototype provides the foundation for a massively parallel GPU-based unification engine, which we plan to develop in future work.
Matching logic is a general formal framework for reasoning about a wide range of theories, with particular emphasis on programming language semantics. Semantic reasoning, such as proof of satisfaction, requires the logic to be expressed within a foundational theory; adopting a dependently typed setting enables well-sortedness in the object theory to correspond directly to well-typedness in the host theory. In this paper, we present the first dependently typed, locally nameless definition of matching μ-logic, including both syntax and semantics, ensuring well-sortedness and local closedness via sorted contexts encoded in type indices. As a result, ill-sorted syntax is unrepresentable, and the semantics of well-sorted elements are guaranteed to lie within the domains of their associated sorts. We also demonstrate how this encoding facilitates model-theoretic reasoning about the consistency of matching logic theories.
AI planning is the task of finding a sequence of actions for a declaratively described system to reach some goal, while (optionally) optimizing some measures. In its classical version, the initial state is fully known and actions have deterministic, known effects. Besides its conceptual simplicity, classical planning is PSPACE-complete, both for satisficing and optimal planning and, consequently, a plethora of heuristic planners do exist, coping with the inherent complexity of the problem in different ways. Nevertheless, SAT based exact methods are competitive with heuristic methods for classical planning in many cases. Several declarative languages have been proposed for classical planning, such as STRIPS or PDDL, with PDDL being the de facto standard that most planners support, at least to some extent. PDDL formulations contain first-order formulas that are usually grounded in order to solve the planning problem, either with heuristic or exact methods, sometimes leading to a blow-up that makes the resulting problem instance intractable. With this in mind, in this paper we present a study on the translation of PDDL formulations to lifted representations in SMT, with the aim of obtaining more compact and, at the same time, efficient formulations for classical planning. We show that SMT formulations often outperform SAT based ones on hard-to-ground instances.
Online stores often include a customer reviews section on their product web pages. These reviews contain valuable information for product sellers, who often want to collect the reviews of their products from as many pages as possible. This work presents a novel technique to automatically extract customer reviews from online stores. Unlike traditional scraping tools, the proposed technique operates on heterogeneous web pages without requiring prior knowledge of their structure or human intervention. By analysing the web page’s DOM tree, it identifies the reviews section, enabling the extraction of text-based comments as well as associated media content such as images and videos. The technique processes individual pages in real time, making it suitable for dynamic browsing scenarios, and has been empirically evaluated on diverse real-world web pages, demonstrating its robustness and versatility. This evaluation shows that the technique achieves an average F1 score of 91.54% and reaches 100% in 82.6% of the web pages.
We propose a 'Model to Mitigate' methodology: designing a platform-agnostic model of smart contract business logic and analyzing it before implementation. Using Dynamic Condition Response (DCR) graphs, originally developed for modeling business processes, we formally specify smart contracts and introduce a trace-conformance notion that links DCR-level guarantees to Solidity execution traces. Our method captures high-level properties such as event ordering, role-based access control, and time constraints, enabling the identification of design-rooted vulnerabilities through the discipline of explicit modeling. The DCR formalism requires developers to make concrete decisions about access control, preconditions, initial states, and event ordering-decisions that, when left implicit until implementation, are a documented source of vulnerabilities. Our analysis of real-world exploited and audited smart contracts yields six key insights, demonstrating how DCR-based modeling can enhance smart contract security by surfacing design flaws before they reach deployment. While we validate the approach on existing smart contracts with known flaws (i. e., post-implementation scenarios), the proposed methodology is applicable during design time (pre-development) .
We investigate methods to automatically derive decision procedures for array theories using expressive features such as unbounded quantification or cardinality constraints from decision procedures for their indices and element theories. We observe that traditional methods such as the Nelson-Oppen combination procedure are severely limited in terms of the theories that can be used to specify elements or indices. We show that the polite theory combination method is already able to combine arbitrary element theories with theories of sets with cardinality constraints, which was left open in [1]. We also show that the polite theory combination approach is applicable for theories that mix set- and first-order specifications, provided that their signatures are disjoint. Finally, we show that for fragments with non-disjoint signatures, a reduction approach can be used to modularly combine arbitrary index and element theories. Our results provide a starting point for the analysis of the modular combination problem of expressive string or sequence theories.
Pattern completeness is the property that the left-hand sides of a functional program cover all cases w.r.t. pattern matching. In the context of term rewriting a related notion is quasi-reducibility, a prerequisite if one wants to perform ground confluence proofs by rewriting induction.In order to certify such confluence proofs, we develop a novel algorithm that decides pattern completeness and that can be used to ensure quasi-reducibility. One of the advantages of the proposed algorithm is its simple structure: it is similar to that of a regular matching algorithm and, unlike an existing decision procedure for quasi-reducibility, it avoids enumerating all terms up to a given depth. The algorithm has an asymptotic optimal complexity, as it exhibits a co-NP behavior.Despite the simple structure, it is not immediate to either prove the correctness of the algorithm or the co-NP behavior. Therefore we formalize the algorithm and verify its correctness using the proof assistant Isabelle/HOL. To this end, we not only verify some auxiliary algorithms, but also design an Isabelle library on sorted term rewriting. Moreover, we export the verified code in Haskell and experimentally evaluate its performance. We observe that our algorithm significantly outperforms existing algorithms, even including the pattern completeness check of the GHC Haskell compiler.
Programmable logic controllers (PLCs) are widely used in diverse industrial applications. Ensuring the correctness of PLC programs is very important due to their safety-critical nature. Structured text (ST) is an imperative programming language for PLC. Despite recent advances in executable semantics of PLC ST, existing methods neglect complex multitasking and preemption features. This paper presents a rewriting-based executable semantics of PLC ST with preemptive multitasking. Formal analysis of multitasking programs, however, suffers from the state explosion problem. To mitigate this problem, we also propose state space reduction techniques for model checking multitask PLC ST programs. Building on these foundations, we apply rewriting modulo SMT to symbolically analyze LTL properties of multitasking PLC ST programs over finite traces of (possibly infinite) inputs and outputs. We have integrated our techniques into the STbmc tool, a bounded model checker for PLC ST programs originally developed for single-task programs.
Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern in normal form is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. The number of structural components can be reduced by unification and anti-unification. Algorithms for both processes have already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language, while generalizing the unification problem and mechanizing a proven-sound solution in Coq, as well as exploring certain possible extensions of the unification algorithm in a semi-formalized manner.
This paper studies algorithms implementing the Discrete Fourier Transformation in various contexts including digital signal processing, cryptography, and quantum computing. These algorithms are unified under a single model that extends the abstraction of the Fast Fourier Transformation (FFT) as a ring isomorphism. This model provides a single common structure inherent to a wide range FFT algorithms despite their unique algebraic derivations. Using such a model we verify the design of these algorithms with static analysis, contrast their structures, and provide a foundation for synthesizing such programs. We show this method is theoretically well founded insofar as it excludes trivially inefficient algorithms and guarantees the correctness of the algorithms expressed within it. This work began as an attempt to use the ring isomorphism abstraction to improve existing Fourier algorithms. We did not find any improvements by hand, but found a useful formalism of these algorithms along the way. So far as this work is concerned, there is nothing new under the sum.
