A general setting for flexibly combining and augmenting decision procedures

DOI10.1023/A:1015707001763MaRDI QIDQ1610671zbMATH OpenOpenAlexFDO

Authors Predrag Janičić, Alan Bundy

Publication date 20 August 2002

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

Full work available at URL https://doi.org/10.1023/a:1015707001763

zbMATH Keywords

theorem provingefficient combining and augmenting of decision procedures

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 2086596
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 1956606
• Strategies for combining decision procedures
• scientific article; zbMATH DE number 4029278
• scientific article; zbMATH DE number 1149811
• Combining decision procedures by (model-)equality propagation
• Combining Decision Procedures by (Model-)Equality Propagation
• Augmentation and synthesis of knowledge in problems of decision-making theory
• Combining decision procedures for the reals

Cited in

(5)

• Learning strategies for mechanised building of decision procedures
• Model-theoretic methods in combined constraint satisfiability
• An integrated approach to high integrity software verification
• Strategies for combining decision procedures
• Quantifier Elimination and Provers Integration

Describes a project that uses

Uses Software

• PVS

This page was built for publication: A general setting for flexibly combining and augmenting decision procedures

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