Constraints and theorem proving

DOI10.1007/3-540-45406-3_4MaRDI QIDQ2762631zbMATH OpenFDO

Authors Harald Ganzinger, Robert Nieuwenhuis

Publication date 9 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2002/2002159.

Mathematics Subject Classification ID

Logic in computer science (03B70)

Review text

Symbolic constraints provide a convenient way of describing the connection between deduction at the level of ground formulae and the general inferences as they are computed by a prover on formulae with variables. For the entire collection see [Zbl 0961.00024].

Recommendations

• Connection tableau calculi with disjunctive contraints (TU München)
• scientific article; zbMATH DE number 7680806
• scientific article; zbMATH DE number 549980
• Theorem proving with ordering and equality constrained clauses
• Constrained equational deduction

Cited in

(10)

• Constraints, consistency and closure
• On generalized constraints and certificates
• Generalized rewrite theories, coherence completion, and symbolic methods
• p-constraint and the transitivity theorem
• Constraints in non-Boolean contexts
• Rewriting modulo SMT and open system analysis
• Harald Ganzinger's legacy: contributions to logics and programming
• AI*IA 2005: Advances in Artificial Intelligence
• Constrained equational deduction
• Partial redundancy in saturation

Describes a project that uses

Uses Software

• Saturate

This page was built for publication: Constraints and theorem proving

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