More Like this

1. Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties

   https://doi.org/10.46298/lmcs-19(1:19)2023  

   Kapur, Deepak (March 2023, Logical Methods in Computer Science)

   Algorithms for computing congruence closure of ground equations overuninterpreted symbols and interpreted symbols satisfying associativity andcommutativity (AC) properties are proposed. The algorithms are based on aframework for computing a congruence closure by abstracting nonflat terms byconstants as proposed first in Kapur's congruence closure algorithm (RTA97).The framework is general, flexible, and has been extended also to developcongruence closure algorithms for the cases when associative-commutativefunction symbols can have additional properties including idempotency,nilpotency, identities, cancellativity and group properties as well as theirvarious combinations. Algorithms are modular; their correctness and terminationproofs are simple, exploiting modularity. Unlike earlier algorithms, theproposed algorithms neither rely on complex AC compatible well-foundedorderings on nonvariable terms nor need to use the associative-commutativeunification and extension rules in completion for generating canonical rewritesystems for congruence closures. They are particularly suited for integratinginto the Satisfiability modulo Theories (SMT) solvers. A new way to viewGroebner basis algorithm for polynomial ideals with integer coefficients as acombination of the congruence closures over the AC symbol * with the identity 1and the congruence closure over an Abelian group with + is outlined. 

   more » « less
2. Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols

   https://doi.org/10.1007/s10817-022-09624-4  

   Baader, Franz; Kapur, Deepak (August 2022, Journal of Automated Reasoning)

   Abstract The word problem for a finite set of ground identities is known to be decidable in polynomial time using congruence closure, and this is also the case if some of the function symbols are assumed to be commutative or defined by certain shallow identities, called strongly shallow. We show that decidability in P is preserved if we add the assumption that certain function symbolsfareextensionalin the sense that$$f(s_1,\ldots ,s_n) \mathrel {\approx }f(t_1,\ldots ,t_n)$$ $f(s_1,\dots ,s_n)\approx f(t_1,\dots ,t_n)$implies$$s_1 \mathrel {\approx }t_1,\ldots ,s_n \mathrel {\approx }t_n$$ $s_1\approx t_1,\dots ,s_n\approx t_n$. In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP. 

   more » « less
3. Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations

   Ghilardi, Silvio; Gianola, Alessandro; Kapur, Deepak (July 2020, Unknown)

   The concept of a uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the formal methods and automated reasoning community. This concept is precisely defined. Two algorithms for computing the uniform interpolant of a quantifier-free formula in EUF endowed with a list of symbols to be eliminated are proposed. The first algorithm is non-deterministic and generates a uniform interpolant expressed as a disjunction of conjunction of literals, whereas the second algorithm gives a compact representation of a uniform interpolant as a conjunction of Horn clauses. Both algorithms exploit efficient dedicated DAG representations of terms. Correctness and completeness proofs are supplied, using arguments combining rewrite techniques with model theory. 

   more » « less
4. Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations

   Ghilardi, Silvio; Gianola, Alessandro; Kapur, Deepak (October 2020, Unknown)

   The concept of a uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the formal methods and automated reasoning community. This concept is precisely defined. Two algorithms for computing the uniform interpolant of a quantifier-free formula in EUF endowed with a list of symbols to be eliminated are proposed. The first algorithm is non-deterministic and generates a uniform interpolant expressed as a disjunction of conjunction of literals, whereas the second algorithm gives a compact representation of a uniform interpolant as a conjunction of Horn clauses. Both algorithms exploit efficient dedicated DAG representations of terms. Correctness and completeness proofs are supplied, using arguments combining rewrite techniques with model theory. 

   more » « less
5. Experimenting with Symplectic Hypergeometric Monodromy Groups

   https://doi.org/10.1080/10586458.2020.1780516  

   Detinko, A. S.; Flannery, D. L.; Hulpke, A. (June 2020, Experimental Mathematics)

   We present new computational results for symplectic monodromy groups of hypergeometric dif- ferential equations. In particular, we compute the arithmetic closure of each group, sometimes jus- tifying arithmeticity. The results are obtained by extending our earlier algorithms for Zariski dense groups, based on the strong approximation and congruence subgroup properties. 

   more » « less