Equational theorem proving for clauses over strings

DOI10.1017/S0960129524000112MaRDI QIDQ7020356zbMATH OpenFDO

Authors Dohan Kim

Publication date 4 March 2025

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1017/S0960129524000112

zbMATH Keywords

conditional completionequational theorem provingstring rewritingsuperposition calculusunification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A completion procedure for finitely presented groups that is based on word cycles
• A rewriting approach to satisfiability procedures.
• An efficient SMT solver for string constraints
• Complete sets of transformations for general E-unification
• Conditional semi-Thue systems for presenting monoids
• Cross-sections for finitely presented monoids with decidable word problems
• Equational Theorem Proving for Clauses over Strings
• Equational theorem proving modulo
• Equational unification, word unification, and 2nd-order equational unification
• scientific article; zbMATH DE number 53661 (Why is no real title available?)
• scientific article; zbMATH DE number 176740 (Why is no real title available?)
• scientific article; zbMATH DE number 176741 (Why is no real title available?)
• scientific article; zbMATH DE number 1980932 (Why is no real title available?)
• scientific article; zbMATH DE number 1552532 (Why is no real title available?)
• scientific article; zbMATH DE number 2133330 (Why is no real title available?)
• scientific article; zbMATH DE number 789389 (Why is no real title available?)
• Introduction to algorithms
• Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
• ON PRESENTATIONS OF COMMUTATIVE MONOIDS
• Paramodulation-based theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Rewriting
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Testing for the Church-Rosser property
• The Knuth-Bendix Completion Procedure and Thue Systems
• Theorem proving modulo associativity
• Unification and matching modulo nilpotence
• Unification theory
• Variants and satisfiability in the infinitary unification wonderland

Cited in

(1)

• An Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems

This page was built for publication: Equational theorem proving for clauses over strings

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