Modular instantiation schemes

Instantiation schemes are proof procedures that test the satisfiability of clause sets by instantiating the variables they contain, and testing the satisfiability of the resulting ground set of clauses. Such schemes have been devised for several theories, including fragments of linear arithmetic or...

Full description

Saved in:
Bibliographic Details
Published in:Information processing letters 2011-10, Vol.111 (20), p.989-993
Main Authors: Echenim, Mnacho, Peltier, Nicolas
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Arithmetic
Automatic theorem proving
Combination problems
Computer Science
Computer science
control theory
systems
Data processing. List processing. Character string processing
Exact sciences and technology
Fragments
Grounds
Instantiation-based methods
Logic in Computer Science
Mathematical problems
Memory organisation. Data processing
Miscellaneous
Modular
Proof theory
Proving
SMT
Software
Studies
Theoretical computing
Unions
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Instantiation schemes are proof procedures that test the satisfiability of clause sets by instantiating the variables they contain, and testing the satisfiability of the resulting ground set of clauses. Such schemes have been devised for several theories, including fragments of linear arithmetic or theories of data-structures. In this paper we investigate under what conditions instantiation schemes can be combined to solve satisfiability problems in unions of theories. ► A method is introduced for automatically combining instantiation schemes for unions of theories. ► Sufficient conditions are devised to ensure refutational completeness. ► Existing instantiation procedures are adapted to fulfill the considered requirements. ► Some examples of applications are provided.
ISSN:0020-0190
1872-6119
DOI:10.1016/j.ipl.2011.07.003