Constraint solving for proof planning

DOI10.1007/s10817-004-2725-6zbMath1071.68093OpenAlexW1979721470MaRDI QIDQ1774557

Jürgen Zimmer, Erica Melis

Publication date: 17 May 2005

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-004-2725-6

zbMATH Keywords

automated reasoningconstraint satisfactionproof plans

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Proof planning with multiple strategies, Computer supported mathematics with \(\Omega\)MEGA

Uses Software

• Mathematica
• OTTER
• TPTP
• Mozart
• Oz
• MathWeb
• Mathpert

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• Challenge problems in elementary calculus
• Network-based heuristics for constraint-satisfaction problems
• A theory of abstraction
• Consistency in networks of relations
• The TPTP problem library. CNF release v1. 2. 1
• A resolution principle for constrained logics
• The Heine-Borel challenge problem. In honor of Woody Bledsoe
• Comparing approaches to the exploration of the domain of residue classes.
• Automated deduction by theory resolution
• Knowledge-based proof planning
• STRIPS: A new approach to the application of theorem proving to problem solving
• Computer proofs of limit theorems
• Combining linear programming and satisfiability solving for resource planning
• New methods to color the vertices of a graph
• Term Rewriting and All That