Constraint logic: unification and resolution

Got it! This site "creationpie.com" uses cookies. You consent to this by clicking on "Got it!" or by continuing to use this website. Note: This appears on each machine/browser from which this site is accessed.

A constraint logic system is a system of constraints whose solution needs to satisfy those constraints.

A unifier unifies the constraints without contradictions.

A MGU (Most General Unifier) unifies the constraints without contradictions and has a minimal frontier in the lattice of constraints, a LFP (Least Fixed Point).

If there are multiple solutions, a constraint logic system will attempt to find all MGU constraints.

In logical reasoning terms, this uses a "negation by failure" reasoning, common in logical programming and in human logic.

Negation by failure goes as follows: If one cannot prove something true it is assumed to be false.

If something cannot be shown to be a witness for God, then it is, by negation by failure reasoning, a sin.

Determining the meaning of a word or phrase or idiom by looking at how it is used is similar to the idea of unification in computer science (type inference) or logic programming (e.g., Prolog) or constraint logic programming in general.

Robinson's unification algorithm (1965)
Hindley-Milner type inference (1969, 1978)

A unifier solves a problem for the entire collection of examples. A MGU is more general than any other unifier.

The goal, as in programming, is to find the least fixed point of a system of constraints that will act as a MGU. This is more complicated, linguistically, when there is more than one word or phrase that is unknown in all examples of text that use that word or phrase.

A specific implementation of unification and resolution is found in the logic programming language Prolog which stands for "Programming in logic". Prolog uses "logical variables" which are placeholders to be filled-in later. Backtracking allows Prolog to undo assumptions when no solution is possible in order to try to find a solution or more solutions.

More: Prolog: Logical variables

Unification A solution to a query is a binding to variables that make the query true (satisfy it). Unification is the minimal substitution of terms for variables such that the terms are satisfied.

In a logic language, such as Prolog, a logical variable is a placeholder that can hold one value. If at some point the system cannot be unified, backtracking is done to find a point at which the search for a solution can continue.

In this example, a logical variable is used to represent "salt". That is, whatever "salt" represents. And so on.

Let use cover some constraints as they appear and then summarize them at the end. For the present, where the KJV (King James Version) models the GNT (Greek New Testament), we will not be concerned with any nuances.

Unification is a form of finding (similar) pieces of a puzzle given a framework of constraints.

This is, given a selection of texts where all (or most) of the words are known except for one, the goal is to find a unifier such that all of the texts now make sense in the context that they are written.

Some puzzles are easier to solve than other puzzles.


all in	all none	all out

A simple puzzle piece has four sides and each side can have one of three configurations: in, none, out.

There are 3*3*3*3 or 81 possible puzzle pieces. But some are the same under rotation so that there are 24 unique pieces. These 24 pieces can be used to create a puzzle. It is harder to take the mixed-up pieces and make the puzzle.

Find a better word that fits the constraints discussed above. The "Suggest" button provides one possible constraint solution, but not the best one.

Matthew 5:13. Ye are the salt of the earth: but if the salt have lost its saltiness, wherewith shall it be salted? The salt is/are thenceforth good for nothing, but to be cast out, and to be trodden under foot of men.
Mark 9:49. For every one shall be salted with fire.
Mark 9:50. salted is good: but if the salt have lost its saltiness, wherewith will ye salt it? Have salt in yourselves, and have peace one with another.
Colossians 4:6. Let your speech be always with grace, salted with salt, that ye may know how ye ought to answer every man.