Extending Maximal Completion (Invited Talk)

DOI10.4230/LIPIcs.FSCD.2019.3OpenAlexW2955328239MaRDI QIDQ5089002

Sarah Winkler

Publication date: 18 July 2022

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2019/10510/pdf/LIPIcs-FSCD-2019-3.pdf/

zbMATH Keywords

theorem provingautomated reasoningcompletion

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Termination and completion modulo associativity, commutativity and identity
• Completion for rewriting modulo a congruence
• A fully syntactic AC-RPO.
• On using ground joinable equations in equational theorem proving
• MædMax: a maximal ordered completion tool
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• System Description: E 1.8
• Taking Satisfiability to the Next Level with Z3
• Abstract conflict driven learning
• Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• Algebraic data integration
• Term Rewriting and All That
• Conditional Confluence (System Description)
• Automated Reasoning
• Linear completion

This page was built for publication: Extending Maximal Completion (Invited Talk)