On Combining Theories with Shared Set Operations

We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas obtained by applying propositional operations to quantified formulas belonging to several expressive decidable logics.


Year:
2009
Laboratories:




 Record created 2009-05-09, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)