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.


    • LARA-REPORT-2009-002

    Record created on 2009-05-09, modified on 2017-05-12

Related material