**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.

Publication# On Combining Theories with Shared Set Operations

Abstract

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.

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (35)

Related concepts (34)

Related MOOCs (3)

Ontological neighbourhood

First-order logic

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.

Decidability of first-order theories of the real numbers

In mathematical logic, a first-order language of the real numbers is the set of all well-formed sentences of first-order logic that involve universal and existential quantifiers and logical combinations of equalities and inequalities of expressions over real variables. The corresponding first-order theory is the set of sentences that are actually true of the real numbers. There are several different such theories, with different expressive power, depending on the primitive operations that are allowed to be used in the expression.

Decision problem

In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm whether a given natural number is prime. Another is the problem "given two numbers x and y, does x evenly divide y?". The answer is either 'yes' or 'no' depending upon the values of x and y. A method for solving a decision problem, given in the form of an algorithm, is called a decision procedure for that problem.

Parallel programming

With every smartphone and computer now boasting multiple processors, the use of functional ideas to facilitate parallel programming is becoming increasingly widespread. In this course, you'll learn th

Parallel programming

With every smartphone and computer now boasting multiple processors, the use of functional ideas to facilitate parallel programming is becoming increasingly widespread. In this course, you'll learn th

Parallel programming

With every smartphone and computer now boasting multiple processors, the use of functional ideas to facilitate parallel programming is becoming increasingly widespread. In this course, you'll learn th

We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction ...

We study the satisfiability problem of symbolic tree automata and decompose it into the satisfiability problem of the existential first-order theory of the input characters and the existential monadic second-order theory of the indices of the accepted word ...

2023```
We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having po ...
```