Instantiation schemes for nested theories

DOI10.1145/2480759.2480763MaRDI QIDQ2946696zbMATH OpenOpenAlexFDO

Authors Mnacho Echenim, Nicolas Peltier

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1107.4937

zbMATH Keywords

combination of theoriesinstantiation-based proof proceduressatisfiability modulo theories

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: This paper investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures for richer theories. Interesting applications in the field of verification are emphasized, particularly for handling extensions of the theory of arrays.

Recommendations

• Modular instantiation schemes
• Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
• Theory Instantiation
• An instantiation scheme for satisfiability modulo theories
• Instantiation theory. On the foundations of automated deduction

Cited in

(2)

• Modular instantiation schemes
• Theory Instantiation

This page was built for publication: Instantiation schemes for nested theories

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