**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 GraphSearch.

Concept# Decidability (logic)

Summary

In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems are decidable if membership in their set of logically valid formulas (or theorems) can be effectively determined. A theory (set of sentences closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory. Many important problems are undecidable, that is, it has been proven that no effective method for determining membership (returning a correct answer after finite, though possibly very long, time in all cases) can exist for them.
Decidability of a logical system
Each logical system comes with both a syntactic component, which among other things determines the notion of provability, and a semantic component, which determines

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

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related publications (7)

Loading

Loading

Loading

Related people (2)

Related concepts (31)

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

Logic

Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or logical truths. It studies how conclusions follo

Peano axioms

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giusep

Related courses (3)

CS-119(c): Information, Computation, Communication

L'objectif de ce cours est d'introduire les étudiants à la pensée algorithmique, de les familiariser avec les fondamentaux de l'Informatique et de développer une première compétence en programmation (langage C++).

MATH-483: Gödel and recursivity

Gödel incompleteness theorems and mathematical foundations of computer science

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

Related units (1)

Related lectures (5)

We explore the border between decidability and undecidability of verification problems related to message passing systems that admit unbounded creation of threads and name mobility. Inspired by use cases in real-life programs we introduce the notion of depth-bounded message passing systems. A configuration of a message passing system can be represented as a graph. In a depth-bounded system the length of the longest acyclic path in each reachable configuration is bounded by a constant. While the general reachability problem for depth-bounded systems is undecidable, we prove that control reachability is decidable. In our decidability proof we show that depth-bounded systems are well-structured transition systems to which a forward algorithm for the covering problem can be applied.

2009Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.

Mirco Dotta, Viktor Kuncak, Philippe Paul Henri Suter

We describe a parameterized decision procedure that extends the decision procedure for functional recursive algebraic data types (trees) with the ability to specify and reason about abstractions of data structures. The abstract values are specified using recursive abstraction functions that map trees into other data types that have decidable theories. Our result yields a decidable logic which can be used to prove that implementations of functional data structures satisfy recursively specified invariants and conform to interfaces given in terms of sets, multisets, or lists, or to increase the automation in proof assistants.

2009