Metalevel Algorithms for Variant Satisfiability

DOI10.1007/978-3-319-44802-2_10zbMath1367.68256OpenAlexW2513121167MaRDI QIDQ2827841

Stephen Skeirik, José Meseguer

Publication date: 21 October 2016

Published in: Rewriting Logic and Its Applications (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2142/90238

zbMATH Keywords

reflectionMaudefinite variant property (FVP)folding variant narrowingmetalevel algorithmssatisfiability in initial algebras

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Related Items

Metalevel algorithms for variant satisfiability

Uses Software

• Maude
• ITP
• SCC

Cites Work

• Adding decision procedures to SMT solvers using axioms with triggers
• Strict coherence of conditional rewriting modulo axioms
• Complete axiomatizations of some quotient term algebras
• Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Complexity, convexity and combinations of theories
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• A rewriting approach to satisfiability procedures.
• Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
• Folding variant narrowing and optimal variant termination
• Metalevel algorithms for variant satisfiability
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Deciding Combinations of Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Simplification by Cooperating Decision Procedures
• Variant-Based Satisfiability in Initial Algebras
• Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
• A uniform approach to constraint-solving for lists, multisets, compact lists, and sets
• Term Rewriting and Applications
• Term Rewriting and Applications
• Combined Satisfiability Modulo Parametric Theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item