arXiv subjects

Temur Kutsia

Publications and source records attributed to Temur Kutsia.

17 recordsLinked to original sources

arXiv2026

Anti-Unification Completeness Analysis in PVS

In syntactic anti-unification, one is concerned with finding the commonalities between terms, while (uniformly) abstracting their differences. The original goal of anti-unification development in the seventies was to automate inductive reasoning. Recent applications of anti-unification techniques include efficiently transforming sequential code into parallel code, detecting code clones, and preventing software failures. Previous work addressed the elements required to verify, in the Prototype Verification System (PVS), termination and soundness of a functional algorithm based on inference rules for syntactic anti-unification. This paper dissects all aspects required to formally establish the completeness of the rule-based algorithm, highlighting the significant differences in the formalizations of anti-unification and unification.

cs.LO↗

arXiv2025

Generalization of Variadic Structures with Binders: A Tool for Structural Code Comparison

This paper introduces a novel anti-unification algorithm for the generalization of variadic structures with binders, designed as a flexible tool for structural code comparison. By combining nominal techniques for handling variable binding with support for variadic expressions (common in abstract syntax trees and programming languages), the approach addresses key challenges such as overemphasis on bound variable names and difficulty handling insertions or deletions in code fragments. The algorithm distinguishes between atoms and two kinds of variables (term and hedge variables) to compute best generalizations that maximally preserve structural similarities while abstracting systematic differences. It also provides detailed information to reconstruct original expressions and quantify structural differences. This information can be useful in tasks like code clone detection, refactoring, and program analysis. By introducing a parametrizable rigidity function, the technique offers fine-grained control over similarity criteria and reduces nondeterminism, enabling flexible adaptation to practical scenarios where trivial similarities should be discounted. Although demonstrated primarily in the context of code similarity detection, this framework is broadly applicable wherever precise comparison of variadic and binder-rich representations is required.

cs.LO↗

arXiv2025

Graded Quantitative Narrowing

The recently introduced framework of Graded Quantitative Rewriting is an innovative extension of traditional rewriting systems, in which rules are annotated with degrees drawn from a quantale. This framework provides a robust foundation for equational reasoning that incorporates metric aspects, such as the proximity between terms and the complexity of rewriting-based computations. Quantitative narrowing, introduced in this paper, generalizes quantitative rewriting by replacing matching with unification in reduction steps, enabling the reduction of terms even when they contain variables, through simultaneous instantiation and rewriting. In the standard (non-quantitative) setting, narrowing has been successfully applied in various domains, including functional logic programming, theorem proving, and equational unification. Here, we focus on quantitative narrowing to solve unification problems in quantitative equational theories over Lawverean quantales. We establish its soundness and discuss conditions under which completeness can be ensured. This approach allows us to solve quantitative equations in richer theories than those addressed by previous methods.

cs.LO↗

arXiv2025

Higher-Order Pattern Unification Modulo Similarity Relations

The combination of higher-order theories and fuzzy logic can be useful in decision-making tasks that involve reasoning across abstract functions and predicates, where exact matches are often rare or unnecessary. Developing efficient reasoning and computational techniques for such a combined formalism presents a significant challenge. In this paper, we adopt a more straightforward approach aiming at integrating two well-established and computationally well-behaved components: higher-order patterns on one side and fuzzy equivalences expressed through similarity relations based on minimum T-norm on the other. We propose a unification algorithm for higher-order patterns modulo these similarity relations and prove its termination, soundness, and completeness. This unification problem, like its crisp counterpart, is unitary. The algorithm computes a most general unifier with the highest degree of approximation when the given terms are unifiable.

cs.AI↗

arXiv2025

Nominal anti-unification

We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and $\alpha$-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems were generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.

cs.LO↗

arXiv2025

Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories

Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints. These problems often lack a least general solution. However, leveraging nominal techniques, we previously demonstrated that a semantic approach with atom-variables enables the elimination of redundant solutions and allows for computing unique least general generalizations (LGGs). In this work, we extend this approach to handle associative (A), commutative (C), and associative-commutative (AC) equational theories. We present a sound and weak complete algorithm for solving equational generalization problems, which generates finite weak minimal complete sets of LGGs for each theory. A key challenge arises from solving equivariance problems while taking into account these equational theories, as identifying redundant generalizations requires recognizing when one expression (with binders) is a renaming of another while possibly considering permutations of sub-expressions. This unexpected interaction between renaming and equational reasoning made this particularly difficult, necessitating semantic tests within the equivariance algorithm. Given that these equational theories naturally induce exponentially large LGG sets due to subexpression permutations, future work could explore restricted theory fragments where the generalization problem remains unitary. In these fragments, LGGs can be computed efficiently in polynomial time, offering practical benefits for symbolic computation and automated reasoning tasks.

cs.LO↗

arXiv2024

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis

This volume contains * The post-proceedings of the Eighteenth Logical and Semantic Frameworks with Applications (LSFA 2023). The meeting was held on July 1-2, 2023, organised by the Sapienza Università di Roma, Italy. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include proof theory, type theory and rewriting theory, specification and deduction languages, and formal semantics of languages and systems. * The post-proceedings of the Tenth Workshop on Horn clauses for Verification and Synthesis (HCVS 2023). The meeting was held on April 23, 2023 at the Institut Henri Poincaré in Paris. HCVS aims to bring together researchers working in the two communities of constraint/ logic programming (e.g., ICLP and CP), program verification (e.g., CAV, TACAS, and VMCAI), and automated deduction (e.g., CADE, IJCAR), on the topics of Horn clause based analysis, verification, and synthesis.

cs.LO↗

arXiv2023

Equational Anti-Unification over Absorption Theories

Interest in anti-unification, the dual problem of unification, is on the rise due to applications within the field of software analysis and related areas. For example, anti-unification-based techniques have found uses within clone detection and automatic program repair methods. While syntactic forms of anti-unification are enough for many applications, some aspects of software analysis methods are more appropriately modeled by reasoning modulo an equational theory. Thus, extending existing anti-unification methods to deal with important equational theories is the natural step forward. This paper considers anti-unification modulo pure absorption theories, i.e., some operators are associated with a special constant satisfying the axiom $f(x,\varepsilon_f) \approx f(\varepsilon_f,x) \approx \varepsilon_f$. We provide a sound and complete rule-based algorithm for such theories. Furthermore, we show that anti-unification modulo absorption is infinitary. Despite this, our algorithm terminates and produces a finitary algorithmic representation of the minimal complete set of solutions. We also show that the linear variant is finitary.

cs.LO↗

arXiv2023

Enumerating All Maximal Clique-Partitions of an Undirected Graph

We address the problem of enumerating all maximal clique-partitions of an undirected graph and present an algorithm based on the observation that every maximal clique-partition can be produced from the maximal clique-cover of the graph by assigning the vertices shared among maximal cliques, to belong to only one clique. This simple algorithm has the following drawbacks: (1) the search space is very large; (2) it finds some clique-partitions which are not maximal; and (3) some clique-partitions are found more than once. We propose two criteria to avoid these drawbacks. The outcome is an algorithm that explores a much smaller search space and guarantees that every maximal clique-partition is computed only once. The algorithm can be used in problems such as anti-unification with proximity relations or in resource allocation tasks when one looks for several alternative ways to allocate resources.

cs.DM↗

arXiv2023

Anti-unification and Generalization: A Survey

Anti-unification (AU) is a fundamental operation for generalization computation used for inductive inference. It is the dual operation to unification, an operation at the foundation of automated theorem proving. Interest in AU from the AI and related communities is growing, but without a systematic study of the concept nor surveys of existing work, investigations often resort to developing application-specific methods that existing approaches may cover. We provide the first survey of AU research and its applications and a general framework for categorizing existing and future developments.

cs.LO↗

arXiv2022

Nominal Unification and Matching of Higher Order Expressions with Recursive Let

A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expressions with recursive let and atom-variables, where we show that it also runs in nondeterministic polynomial time. In addition we prove that there is a guessing strategy for nominal unification with letrec and atom-variable that is a trade-off between exponential growth and non-determinism. Nominal matching with variables representing partial letrec-environments is also shown to be in NP.

cs.LO↗

arXiv2021

Proceedings of the 9th International Symposium on Symbolic Computation in Software Science

This volume contains papers presented at the Ninth International Symposium on Symbolic Computation in Software Science, SCSS 2021. Symbolic Computation is the science of computing with symbolic objects (terms, formulae, programs, representations of algebraic objects, etc.). Powerful algorithms have been developed during the past decades for the major subareas of symbolic computation: computer algebra and computational logic. These algorithms and methods are successfully applied in various fields, including software science, which covers a broad range of topics about software construction and analysis. Meanwhile, artificial intelligence methods and machine learning algorithms are widely used nowadays in various domains and, in particular, combined with symbolic computation. Several approaches mix artificial intelligence and symbolic methods and tools deployed over large corpora to create what is known as cognitive systems. Cognitive computing focuses on building systems that interact with humans naturally by reasoning, aiming at learning at scale. The purpose of SCSS is to promote research on theoretical and practical aspects of symbolic computation in software science, combined with modern artificial intelligence techniques. These proceedings contain the keynote paper by Bruno Buchberger and ten contributed papers. Besides, the conference program included three invited talks, nine short and work-in-progress papers, and a special session on computer algebra and computational logic. Due to the COVID-19 pandemic, the symposium was held completely online. It was organized by the Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University Linz on September 8--10, 2021.

cs.SC↗

arXiv2018

Higher-Order Equational Pattern Anti-Unification [Preprint]

We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of generalizations contains finitely many elements. We define the notion of optimal solution and investigate special fragments of the problem for which the optimal solution can be computed in linear or polynomial time.

cs.LO↗

arXiv2017

MK-fuzzy Automata and MSO Logics

We introduce MK-fuzzy automata over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applications being in development in a project on runtime network monitoring based on predicate logic. We investigate closure properties of the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well as of deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts. Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce an MK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzy automata, i.e., a Büchi type theorem.

cs.FL↗

arXiv2016

Nominal Unification of Higher Order Expressions with Recursive Let

A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine the complexity of corresponding unification problems.

cs.PL↗

arXiv2015

CLP(H): Constraint Logic Programming for Hedges

CLP(H) is an instantiation of the general constraint logic programming scheme with the constraint domain of hedges. Hedges are finite sequences of unranked terms, built over variadic function symbols and three kinds of variables: for terms, for hedges, and for function symbols. Constraints involve equations between unranked terms and atoms for regular hedge language membership. We study algebraic semantics of CLP(H) programs, define a sound, terminating, and incomplete constraint solver, investigate two fragments of constraints for which the solver returns a complete set of solutions, and describe classes of programs that generate such constraints.

cs.LO↗

arXiv2010

Strategies in PRholog

PRholog is an experimental extension of logic programming with strategic conditional transformation rules, combining Prolog with Rholog calculus. The rules perform nondeterministic transformations on hedges. Queries may have several results that can be explored on backtracking. Strategies provide a control on rule applications in a declarative way. With strategy combinators, the user can construct more complex strategies from simpler ones. Matching with four different kinds of variables provides a flexible mechanism of selecting (sub)terms during execution. We give an overview on programming with strategies in PRholog and demonstrate how rewriting strategies can be expressed.

cs.PL↗