Paper Info
Title
Schemata of SMT-problems
Abstract
A logic is devised for reasoning about iterated schemata of SMT problems. The satisfiability problem is shown to be undecidable for this logic, but we present a proof procedure that is sound, complete w.r.t. satisfiability and terminating for a precisely characterized class of problems. It is parameterized by an external procedure (used as a black box) for testing the satisfiability of ground instances of the schema in the considered theory (e.g. integers, reals etc.).
Year
DOI
Venue
2011
10.1007/978-3-642-22119-4_5
TABLEAUX
Keywords
Field
DocType
satisfiability problem,smt problem,ground instance,considered theory,complete w,proof procedure,black box,iterated schema,external procedure
Black box (phreaking),Discrete mathematics,Parameterized complexity,Computer science,Satisfiability,Boolean satisfiability problem,Algorithm,Proof procedure,Iterated function,Schema (psychology),Undecidable problem
Conference
Volume
ISSN
Citations 
6793
0302-9743
5
PageRank 
References 
Authors
0.49
7
2
Name
Order
Citations
PageRank
Vincent Aravantinos18610.29
Nicolas Peltier25011.84