Variant-Based Satisfiability in Initial Algebras
From MaRDI portal
Publication:4686604
DOI10.1007/978-3-319-29510-7_1zbMath1396.68074OpenAlexW2294297515MaRDI QIDQ4686604
No author found.
Publication date: 2 October 2018
Published in: Communications in Computer and Information Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-29510-7_1
finite variant property (FVP)folding variant narrowingsatisfiability in initial algebrasconstructor unifierconstructor variant
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (21)
Non-disjoint combined unification and closure by equational paramodulation ⋮ Equational formulas and pattern operations in initial order-sorted algebras ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Metalevel algorithms for variant satisfiability ⋮ An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Optimizing Maude programs via program specialization ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ Polite combination of algebraic datatypes ⋮ Politeness for the theory of algebraic datatypes ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Symbolic computation in Maude: some tapas ⋮ Terminating non-disjoint combined unification
Uses Software
Cites Work
- Adding decision procedures to SMT solvers using axioms with triggers
- An instantiation scheme for satisfiability modulo theories
- Combination techniques and decision problems for disunification
- Strict coherence of conditional rewriting modulo axioms
- Complete axiomatizations of some quotient term algebras
- Complexity of unification problems with associative-commutative operators
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Termination of narrowing revisited
- Counterexamples to termination for the direct sum of term rewriting systems
- Equational problems and disunification
- Complexity, convexity and combinations of theories
- A proof theory for general unification
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Complete sets of transformations for general E-unification
- Combining unification algorithms
- Equational formulae with membership constraints
- A rewriting approach to satisfiability procedures.
- Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
- Unification in the union of disjoint equational theories: Combining decision procedures
- Modularity in term rewriting revisited
- Folding variant narrowing and optimal variant termination
- On Forward Closure and the Finite Variant Property
- Modular termination of basic narrowing and equational unification
- Automated Verification of Equivalence Properties of Cryptographic Protocols
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Infinite-State Model Checking of LTLR Formulas Using Narrowing
- Automated complexity analysis based on ordered resolution
- Order-Sorted Parameterization and Induction
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Solving SAT and SAT Modulo Theories
- Automatic Decidability and Combinability Revisited
- Deciding Combinations of Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Institutions: abstract model theory for specification and programming
- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
- Folding Variant Narrowing and Optimal Variant Termination
- A uniform approach to constraint-solving for lists, multisets, compact lists, and sets
- New results on rewrite-based satisfiability procedures
- Logics in Artificial Intelligence
- Theoretical Aspects of Computing – ICTAC 2005
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- Term Rewriting and Applications
- Term Rewriting and Applications
- Mechanizing Mathematical Reasoning
- Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras
- Combined Satisfiability Modulo Parametric Theories
- Computer Aided Verification
- Automated Deduction – CADE-19
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Variant-Based Satisfiability in Initial Algebras
