Metalevel algorithms for variant satisfiability

DOI10.1007/978-3-319-44802-2_10MaRDI QIDQ2827841zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Metalevel algorithms for variant satisfiability
• Variant-Based Satisfiability in Initial Algebras
• Variant-based decidable satisfiability in initial algebras with predicates
• Variant Satisfiability of Parameterized Strings
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures

Cites work

• scientific article; zbMATH DE number 1688811 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 1337735 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• A rewriting approach to satisfiability procedures.
• A uniform approach to constraint-solving for lists, multisets, compact lists, and sets
• Adding decision procedures to SMT solvers using axioms with triggers
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An abstract decision procedure for a theory of inductive data types.
• Combined Satisfiability Modulo Parametric Theories
• Complete axiomatizations of some quotient term algebras
• Completion of a Set of Rules Modulo a Set of Equations
• Complexity, convexity and combinations of theories
• Constructors, sufficient completeness, and deadlock freedom of rewrite theories
• Deciding Combinations of Theories
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Folding variant narrowing and optimal variant termination
• Metalevel algorithms for variant satisfiability
• Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
• Simplification by Cooperating Decision Procedures
• Strict coherence of conditional rewriting modulo axioms
• Term Rewriting and Applications
• Term Rewriting and Applications
• Variant-Based Satisfiability in Initial Algebras

Cited in

(4)

• Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
• Metalevel algorithms for variant satisfiability
• Variant-based decidable satisfiability in initial algebras with predicates
• Variant-Based Satisfiability in Initial Algebras

Describes a project that uses

Uses Software

• SCC
• ITP
• Maude

This page was built for publication: Metalevel algorithms for variant satisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2827841)