Extending Maximal Completion (Invited Talk)

DOI10.4230/LIPICS.FSCD.2019.3MaRDI QIDQ5089002zbMATH OpenOpenAlexFDO

Authors 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

automated reasoningcompletiontheorem proving

Mathematics Subject Classification ID

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

Recommendations

• Maximal completion
• Completion and reduction orders (invited talk)
• MædMax: a maximal ordered completion tool
• scientific article; zbMATH DE number 4076598
• scientific article; zbMATH DE number 3856444

Cites work

• A fully syntactic AC-RPO.
• Abstract conflict driven learning
• Algebraic data integration
• Automated Reasoning
• Complete Sets of Reductions for Some Equational Theories
• Completion for logically constrained rewriting
• Completion for rewriting modulo a congruence
• Completion of a Set of Rules Modulo a Set of Equations
• Conditional confluence (system description)
• Encoding dependency pair techniques and control strategies for maximal completion
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 1414284 (Why is no real title available?)
• scientific article; zbMATH DE number 7204438 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Linear completion
• Maximal completion
• Mining propositional simplification proofs for small validating clauses
• MædMax: a maximal ordered completion tool
• Normalized completion revisited
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• On using ground joinable equations in equational theorem proving
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• System description: E 1.8
• Taking satisfiability to the next level with Z3 (abstract)
• Term Rewriting and All That
• Termination and completion modulo associativity, commutativity and identity
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Cited in

(4)

• MædMax: a maximal ordered completion tool
• Completion and reduction orders (invited talk)
• Left-Linear Completion with AC Axioms
• Left-linear completion with AC axioms

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

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