Variant-Based Satisfiability in Initial Algebras
From MaRDI portal
Publication:4686604
DOI10.1007/978-3-319-29510-7_1zbMATH Open1396.68074OpenAlexW2294297515MaRDI QIDQ4686604FDOQ4686604
Author name not available (Why is that?)
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
Recommendations
- Variant-based decidable satisfiability in initial algebras with predicates
- Metalevel algorithms for variant satisfiability
- Metalevel algorithms for variant satisfiability
- Variants and satisfiability in the infinitary unification wonderland
- Theory and Applications of Satisfiability Testing
- Variant Satisfiability of Parameterized Strings
- On Some SAT-Variants over Linear Formulas
- [[:Publication:4729350|Title not available (Why is that?)]]
- [[:Publication:4218095|Title not available (Why is that?)]]
- On variable-weighted exact satisfiability problems
finite variant property (FVP)folding variant narrowingsatisfiability in initial algebrasconstructor unifierconstructor variant
Grammars and rewriting systems (68Q42) Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract data types; algebraic specification (68Q65)
Cites Work
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Automated Verification of Equivalence Properties of Cryptographic Protocols
- Title not available (Why is that?)
- Title not available (Why is that?)
- Complexity, convexity and combinations of theories
- Simplification by Cooperating Decision Procedures
- Institutions: abstract model theory for specification and programming
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Solving SAT and SAT Modulo Theories
- Title not available (Why is that?)
- A rewriting approach to satisfiability procedures.
- Adding decision procedures to SMT solvers using axioms with triggers
- New results on rewrite-based satisfiability procedures
- Title not available (Why is that?)
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- Unification in the union of disjoint equational theories: Combining decision procedures
- Fast Decision Procedures Based on Congruence Closure
- Title not available (Why is that?)
- Title not available (Why is that?)
- Complexity of unification problems with associative-commutative operators
- Computer Aided Verification
- Title not available (Why is that?)
- Combining unification algorithms
- Modularity in term rewriting revisited
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Title not available (Why is that?)
- Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
- Term Rewriting and Applications
- Counterexamples to termination for the direct sum of term rewriting systems
- Automated complexity analysis based on ordered resolution
- Automatic Decidability and Combinability Revisited
- Deciding Combinations of Theories
- An instantiation scheme for satisfiability modulo theories
- Logics in Artificial Intelligence
- Equational problems and disunification
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Folding Variant Narrowing and Optimal Variant Termination
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Term Rewriting and Applications
- Completion of a Set of Rules Modulo a Set of Equations
- Theoretical Aspects of Computing – ICTAC 2005
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A proof theory for general unification
- Mechanizing Mathematical Reasoning
- Complete sets of transformations for general E-unification
- Combination techniques and decision problems for disunification
- Folding variant narrowing and optimal variant termination
- Strict coherence of conditional rewriting modulo axioms
- Complete axiomatizations of some quotient term algebras
- Equational formulae with membership constraints
- On Forward Closure and the Finite Variant Property
- Title not available (Why is that?)
- Title not available (Why is that?)
- Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras
- Termination of narrowing revisited
- Combined Satisfiability Modulo Parametric Theories
- Modular termination of basic narrowing and equational unification
- Order-Sorted Parameterization and Induction
- Infinite-State Model Checking of LTLR Formulas Using Narrowing
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A uniform approach to constraint-solving for lists, multisets, compact lists, and sets
- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
- Automated Deduction – CADE-19
Cited In (24)
- Generalized rewrite theories, coherence completion, and symbolic methods
- Symbolic computation in Maude: some tapas
- Non-disjoint combined unification and closure by equational paramodulation
- Equational formulas and pattern operations in initial order-sorted algebras
- 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
- Terminating non-disjoint combined unification
- Optimizing Maude programs via program specialization
- Symbolic Specialization of Rewriting Logic Theories with Presto
- Title not available (Why is that?)
- Title not available (Why is that?)
- An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
- Programming and symbolic computation in Maude
- Optimization of rewrite theories by equational partial evaluation
- Politeness for the theory of algebraic datatypes
- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- Variants and satisfiability in the infinitary unification wonderland
- Checking Sufficient Completeness by Inductive Theorem Proving
- Variant Satisfiability of Parameterized Strings
- Metalevel Algorithms for Variant Satisfiability
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- Polite combination of algebraic datatypes
Uses Software
This page was built for publication: Variant-Based Satisfiability in Initial Algebras
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4686604)
