Constraint contextual rewriting.

DOI10.1016/S0747-7171(03)00025-7MaRDI QIDQ1404984zbMATH OpenFDO

Authors Alessandro Armando, Silvio Ranise

Publication date 25 August 2003

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

decision procedures

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 1538008
• Incorporating decision procedures in implicit induction.
• scientific article; zbMATH DE number 794241
• Implementing contextual rewriting
• Mechanizing Mathematical Reasoning

Cites work

• scientific article; zbMATH DE number 3921957 (Why is no real title available?)
• scientific article; zbMATH DE number 4112064 (Why is no real title available?)
• scientific article; zbMATH DE number 108365 (Why is no real title available?)
• scientific article; zbMATH DE number 1341612 (Why is no real title available?)
• scientific article; zbMATH DE number 1140677 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1765707 (Why is no real title available?)
• scientific article; zbMATH DE number 794241 (Why is no real title available?)
• A practical extension mechanism for decision procedures: The case study of universal Presburger arithmetic
• A practical integration of first-order reasoning and decision procedures
• An overview of the Tecton proof system
• Constraint contextual rewriting.
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• Maple's evaluation process as constraint contextual rewriting
• On Fourier's algorithm for linear arithmetic constraints
• On Shostak's decision procedure for combinations of theories
• Simplification by Cooperating Decision Procedures

Cited in

(9)

• scientific article; zbMATH DE number 1538008 (Why is no real title available?)
• Constraint contextual rewriting.
• Context rewriting
• Subterm contextual rewriting
• scientific article; zbMATH DE number 2090056 (Why is no real title available?)
• Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous
• Maple's evaluation process as constraint contextual rewriting
• Unions of non-disjoint theories and combinations of satisfiability procedures
• A reconstruction and extension of Maple's assume facility via constraint contextual rewriting

Describes a project that uses

Uses Software

• Tecton
• RDL
• STeP
• NQTHM
• OMRS

This page was built for publication: Constraint contextual rewriting.

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