Subterm contextual rewriting

DOI10.3233/AIC-2010-0459MaRDI QIDQ3568223zbMATH OpenFDO

Authors Christoph Weidenbach, Patrick Wischnewski

Publication date 17 June 2010

Published in AI Communications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/AIC-2010-0459

zbMATH Keywords

automated theorem provingrewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 794241
• Implementing contextual rewriting
• Constraint contextual rewriting.
• scientific article; zbMATH DE number 3959369
• scientific article; zbMATH DE number 3930371

Cited in

(10)

• Subsumption demodulation in first-order theorem proving
• SCL(EQ): SCL for first-order logic with equality
• Logical reduction of metarules
• Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous
• scientific article; zbMATH DE number 4050972 (Why is no real title available?)
• scientific article; zbMATH DE number 794241 (Why is no real title available?)
• Harald Ganzinger's legacy: contributions to logics and programming
• Context rewriting
• Implementing contextual rewriting
• SCL(EQ): SCL for first-order logic with equality

Describes a project that uses

Uses Software

• SPASS
• TPTP

This page was built for publication: Subterm contextual rewriting

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