In
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
and
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
, resolution is a
rule of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...
leading to a
refutation complete theorem-proving
A mathematical proof is an Inference, inferential Argument-deduction-proof distinctions, argument for a Proposition, mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previo ...
technique for sentences in
propositional logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
and
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 quantifie ...
. For propositional logic, systematically applying the resolution rule acts as a
decision procedure
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 wheth ...
for formula unsatisfiability, solving the (complement of the)
Boolean satisfiability problem
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
. For
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 quantifie ...
, resolution can be used as the basis for a
semi-algorithm for the unsatisfiability problem of
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 quantifie ...
, providing a more practical method than one following from
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.
The completeness theorem applies to any first-order theory: I ...
.
The resolution rule can be traced back to
Davis
Davis may refer to:
Places Antarctica
* Mount Davis (Antarctica)
* Davis Island (Palmer Archipelago)
* Davis Valley, Queen Elizabeth Land
Canada
* Davis, Saskatchewan, an unincorporated community
* Davis Strait, between Nunavut and Gre ...
and
Putnam (1960); however, their
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
required trying all
ground instance Substitution is a fundamental concept in logic.
A substitution is a syntactic transformation on formal expressions.
To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols by other expressions.
T ...
s of the given formula. This source of combinatorial explosion was eliminated in 1965 by
John Alan Robinson
John Alan Robinson (9 March 1930 – 5 August 2016) was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.
Alan Robinson's major contribution is to the foundations of automated theorem pr ...
's syntactical
unification algorithm In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.
Depending on which expressions (also called ''terms'') are allowed to occur in an equation set (also called ''unification prob ...
, which allowed one to instantiate the formula during the proof "on demand" just as far as needed to keep
refutation completeness
In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula having the property can be derived using that system, i.e. is one of its theorems; otherwise the system is said to be ...
.
The clause produced by a resolution rule is sometimes called a resolvent.
Resolution in propositional logic
Resolution rule
The resolution rule in propositional logic is a single valid inference rule that produces a new clause implied by two
clauses
In language, a clause is a constituent that comprises a semantic predicand (expressed or not) and a semantic predicate. A typical clause consists of a subject and a syntactic predicate, the latter typically a verb phrase composed of a verb with ...
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. It is the principle of ''
consensus'' applied to clauses rather than terms.
When the two clauses contain more than one pair of complementary literals, the resolution rule can be applied (independently) for each such pair; however, the result is always a
tautology.
Modus ponens
In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. ...
can be seen as a special case of resolution (of a one-literal clause and a two-literal clause).
:
is equivalent to
:
A resolution technique
When coupled with a complete
search algorithm
In computer science, a search algorithm is an algorithm designed to solve a search problem. Search algorithms work to retrieve information stored within particular data structure, or calculated in the search space of a problem domain, with eith ...
, the resolution rule yields a
sound
In physics, sound is a vibration that propagates as an acoustic wave, through a transmission medium such as a gas, liquid or solid.
In human physiology and psychology, sound is the ''reception'' of such waves and their ''perception'' by the ...
and
complete
Complete may refer to:
Logic
* Completeness (logic)
* Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable
Mathematics
* The completeness of the real numbers, which implies t ...
algorithm for deciding the ''satisfiability'' of a propositional formula, and, by extension, the
validity
Validity or Valid may refer to:
Science/mathematics/statistics:
* Validity (logic), a property of a logical argument
* Scientific:
** Internal validity, the validity of causal inferences within scientific studies, usually based on experiments
** ...
of a sentence under a set of axioms.
This resolution technique uses
proof by contradiction
In logic and mathematics, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Proof by contradiction is also known as ...
and is based on the fact that any sentence in propositional logic can be transformed into an equivalent sentence in
conjunctive normal form
In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a can ...
.
[ "Before applying the inference method itself, we transform the formulas to quantifier-free conjunctive normal form."] The steps are as follows.
* All sentences in the knowledge base and the ''negation'' of the sentence to be proved (the ''conjecture'') are conjunctively connected.
* The resulting sentence is transformed into a conjunctive normal form with the conjuncts viewed as elements in a set, ''S'', of clauses.
**For example,
gives rise to the set
.
* The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the clause contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set ''S'', it is added to ''S'', and is considered for further resolution inferences.
* If after applying a resolution rule the ''empty clause'' is derived, the original formula is unsatisfiable (or ''contradictory''), and hence it can be concluded that the initial conjecture
follows from the axioms.
* If, on the other hand, the empty clause cannot be derived, and the resolution rule cannot be applied to derive any more new clauses, the conjecture is not a theorem of the original knowledge base.
One instance of this algorithm is the original
Davis–Putnam algorithm The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas ...
that was later refined into the
DPLL algorithm
In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solvi ...
that removed the need for explicit representation of the resolvents.
This description of the resolution technique uses a set ''S'' as the underlying
data-structure to represent resolution derivations.
Lists
A ''list'' is any set of items in a row. List or lists may also refer to:
People
* List (surname)
Organizations
* List College, an undergraduate division of the Jewish Theological Seminary of America
* SC Germania List, German rugby unio ...
,
Trees
In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, including only woody plants with secondary growth, plants that are u ...
and
Directed Acyclic Graph
In mathematics, particularly graph theory, and computer science, a directed acyclic graph (DAG) is a directed graph with no directed cycles. That is, it consists of vertices and edges (also called ''arcs''), with each edge directed from one ve ...
s are other possible and common alternatives. Tree representations are more faithful to the fact that the resolution rule is binary. Together with a sequent notation for clauses, a tree representation also makes it clear to see how the resolution rule is related to a special case of the
cut-rule, restricted to atomic cut-formulas. However, tree representations are not as compact as set or list representations, because they explicitly show redundant subderivations of clauses that are used more than once in the derivation of the empty clause. Graph representations can be as compact in the number of clauses as list representations and they also store structural information regarding which clauses were resolved to derive each resolvent.
A simple example
In plain language: Suppose
is false. In order for the premise
to be true,
must be true.
Alternatively, suppose
is true. In order for the premise
to be true,
must be true. Therefore, regardless of falsehood or veracity of
, if both premises hold, then the conclusion
is true.
Resolution in first-order logic
Resolution rule can be generalized to
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 quantifie ...
to:
:
where
is a
most general unifier In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.
Depending on which expressions (also called ''terms'') are allowed to occur in an equation set (also called ''unification prob ...
of
and
, and
and
have no common variables.
Example
The clauses
and
can apply this rule with