Metalevel algorithms for variant satisfiability

DOI10.1016/j.jlamp.2017.12.006zbMath1430.68423OpenAlexW2791470433WikidataQ130200143 ScholiaQ130200143MaRDI QIDQ2413027

José Meseguer, Stephen Skeirik

Publication date: 6 April 2018

Published in: Journal of Logical and Algebraic Methods in Programming (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) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (8)

Optimization of rewrite theories by equational partial evaluation ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Symbolic computation in Maude: some tapas

Uses Software

• Maude
• ITP
• SCC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Adding decision procedures to SMT solvers using axioms with triggers
• 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.
• Folding variant narrowing and optimal variant termination
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Metalevel Algorithms for Variant Satisfiability
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Termination Modulo Combinations of Equational Theories
• 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
• All-Path Reachability Logic
• Tree generating regular systems
• Term Rewriting and Applications
• Term Rewriting and Applications
• Combined Satisfiability Modulo Parametric Theories

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