resolution
In plain wordsA mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known.
Logic
A rule of inference on clauses (disjunctions of literals): when one clause contains a literal and another contains its negation, the two combine into a resolvent that drops the clashing pair and keeps every other literal from both; in first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI. the clashing literals must first be made identical by unificationunification, n.: Finding values for the blanks in two logical patterns so that they become identical, for example matching 'parent(X, bob)' with 'parent(alice, Y)' by setting X to alice and Y to bob.. Resolution refutation proves that a set of sentences entails a goal by converting the sentences and the negated goal to clause form and deriving the empty clause, a contradiction. The method is refutation-complete: whenever a clause set is unsatisfiable, the empty clause can be derived. Strategies such as set-of-support, literal ordering and subsumption tame the otherwise explosive search. SLD resolution, restricted to Horn clausesHorn clause, n.: A simple, restricted form of logical rule ('if these conditions all hold, then this one conclusion holds') that computers can reason with very efficiently., is the execution mechanism of PrologProlog, prop. n.: A programming language from 1972 in which you state facts and rules in logic and then ask questions; the computer finds answers by searching for proofs., and modern SATBoolean satisfiability problem, n.: The puzzle of deciding whether a set of true-or-false conditions can all be met at once. It is famously hard in theory, yet modern solvers routinely handle millions of conditions. solvers' clause learning is a form of propositional resolution.
Negate the goal, add it to the clauses, and keep resolving until the empty clause appears.
Origin
Introduced by J. Alan Robinson in 'A Machine-Oriented Logic Based on the Resolution Principle' (Journal of the ACM, 1965), building on Herbrand's theorem and on the propositional procedure of Martin Davis and Hilary Putnam (1960). Robert Kowalski's procedural reading of resolution in the early 1970s led to logic programminglogic programming, n.: A style of programming in which you write down facts and rules in logic and then ask questions; the computer works out the answers itself by logical deduction..
Usage note
Unrelated to image or display resolution (pixel count) and to coreference resolution in natural language processing.
Related
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- unificationunification, n.: Finding values for the blanks in two logical patterns so that they become identical, for example matching 'parent(X, bob)' with 'parent(alice, Y)' by setting X to alice and Y to bob.
- first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI.
- Horn clauseHorn clause, n.: A simple, restricted form of logical rule ('if these conditions all hold, then this one conclusion holds') that computers can reason with very efficiently.
- logic programminglogic programming, n.: A style of programming in which you write down facts and rules in logic and then ask questions; the computer works out the answers itself by logical deduction.
- Boolean satisfiability problemBoolean satisfiability problem, n.: The puzzle of deciding whether a set of true-or-false conditions can all be met at once. It is famously hard in theory, yet modern solvers routinely handle millions of conditions.
Sources
- Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1), 23–41.
Mentioned in
automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement., backward chainingbackward chaining, n.: A way of reasoning that starts from the question ('is this true?') and works backward, looking for rules that would prove it and then checking whether their conditions hold., Boolean satisfiability problemBoolean satisfiability problem, n.: The puzzle of deciding whether a set of true-or-false conditions can all be met at once. It is famously hard in theory, yet modern solvers routinely handle millions of conditions., deductive reasoningdeductive reasoning, n.: Reasoning in which true starting points guarantee a true conclusion: if every square is a rectangle and this shape is a square, then it must be a rectangle., first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI., logic programminglogic programming, n.: A style of programming in which you write down facts and rules in logic and then ask questions; the computer works out the answers itself by logical deduction., propositional logicpropositional logic, n.: The simplest formal logic: whole statements that are either true or false, joined by 'and', 'or', 'not' and 'if… then', with exact rules for working out whether the combination is true., Horn clauseHorn clause, n.: A simple, restricted form of logical rule ('if these conditions all hold, then this one conclusion holds') that computers can reason with very efficiently., unificationunification, n.: Finding values for the blanks in two logical patterns so that they become identical, for example matching 'parent(X, bob)' with 'parent(alice, Y)' by setting X to alice and Y to bob.