Resolution (logic) | EPFL Graph Search

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.

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the (complement of the) Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem. The resolution rule can be traced back to Davis and Putnam (1960); however, their algorithm required trying all ground instances of the given formula. This source of combinatorial explosion was eliminated in 1965 by John Alan Robinson's syntactical unification algorithm, which allowed one to instantiate the formula during the proof "on demand" just as far as needed to keep refutation completeness. The clause produced by a resolution rule is sometimes called a resolvent. The resolution rule in propositional logic is a single valid inference rule that produces a new clause implied by two clauses containing complementary literals. A literal is a propositional variable or the negation of a propositional variable. Two literals are said to be complements if one is the negation of the other (in the following, is taken to be the complement to ). The resulting clause contains all the literals that do not have complements. Formally: where all , , and are literals, the dividing line stands for "entails". The above may also be written as: Or schematically as: We have the following terminology: The clauses and are the inference's premises (the resolvent of the premises) is its conclusion. The literal is the left resolved literal, The literal is the right resolved literal, is the resolved atom or pivot. The clause produced by the resolution rule is called the resolvent of the two input clauses.

About this result

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 concepts (24)

Related courses (4)

Related lectures (27)

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 u

EE-431: Advanced VLSI design

In this project-based course, students collect hands-on experience with designing full-custom digital VLSI circuits in dynamic logic. They learn to carry out the design and optimization on transistor

CS-330: Artificial intelligence

Introduction aux techniques de l'Intelligence Artificielle, complémentée par des exercices de programmation qui montrent les algorithmes et des exemples de leur application à des problèmes pratiques.

The superposition calculus is a calculus for reasoning in equational logic. It was developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of (unfailing) Knuth–Bendix completion. It can be seen as a generalization of either resolution (to equational logic) or unfailing completion (to full clausal logic). Like most first-order calculi, superposition tries to show the unsatisfiability of a set of first-order clauses, i.e.

In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form which gives it useful properties for use in logic programming, formal specification, and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951. A Horn clause is a clause (a disjunction of literals) with at most one positive, i.e. unnegated, literal. Conversely, a disjunction of literals with at most one negated literal is called a dual-Horn clause.

Coq: Introduction

Introduces Coq, covering defining propositions, proving theorems, and using tactics.

Inference Engines: Resolution and Horn Clauses CS-330: Artificial intelligence

Covers inference engines based on resolution, Horn clauses, filtering, and unification in artificial intelligence.

Leveling of Slabs: Thickness Calculation ENV-140: Fundamentals of geomatics MOOC: Elements of Geomatics

Covers the principles of leveling and calculations for slab thickness and ceiling height.