Completion-time optimization of rewrite-time goal solving

DOI10.1007/3-540-51081-8_99MaRDI QIDQ5055711zbMATH OpenOpenAlexFDO

Authors Hubert Bertling, Harald Ganzinger

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-51081-8_99

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)

Recommendations

• Goal-directed completion using SOUR graphs
• Maximal completion
• Towards a foundation of completion procedures as semidecision procedures
• Termination by completion
• scientific article; zbMATH DE number 44069

Cites work

• Completion-time optimization of rewrite-time goal solving
• Conditional rewrite rules: Confluence and termination
• Equality, types, modules, and (why not?) generics for logic programming
• scientific article; zbMATH DE number 4016182 (Why is no real title available?)
• scientific article; zbMATH DE number 3930372 (Why is no real title available?)
• scientific article; zbMATH DE number 4031035 (Why is no real title available?)
• scientific article; zbMATH DE number 4053008 (Why is no real title available?)
• scientific article; zbMATH DE number 4064978 (Why is no real title available?)
• scientific article; zbMATH DE number 4078788 (Why is no real title available?)
• scientific article; zbMATH DE number 4090770 (Why is no real title available?)
• scientific article; zbMATH DE number 4090847 (Why is no real title available?)
• scientific article; zbMATH DE number 4090848 (Why is no real title available?)
• scientific article; zbMATH DE number 4090851 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 193539 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• Order-sorted completion: The many-sorted way

Cited in

(12)

• Order-sorted completion: The many-sorted way
• Efficient deduction in equality Horn logic by Horn-completion
• Logicality of conditional rewrite systems
• Shallow confluence of conditional term rewriting systems
• scientific article; zbMATH DE number 4078788 (Why is no real title available?)
• Goal-directed completion using SOUR graphs
• Completion-time optimization of rewrite-time goal solving
• Level-confluence of conditional rewrite systems with extra variables in right-hand sides
• Operational termination of conditional rewriting with built-in numbers and semantic data structures
• Completion of first-order clauses with equality by strict superposition
• Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation
• A rationale for conditional equational programming

This page was built for publication: Completion-time optimization of rewrite-time goal solving

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