Content deleted Content added
→Bottom-up evaluation: termination using entailment |
link to constraint programming |
||
Line 1:
'''Constraint logic programming''' is a
Like in regular logic programming, programs are queried about the provability of a goal. A proof for a goal is composed of clauses whose constraints are satisfied and whose literals can in turn be proved using other clauses. Execution is done by an interpreter, which starts from the goal and [[Recursion|recursively]] scans the clauses trying to prove the goal. Constraints encountered during this scan are placed in a set called '''constraint store'''. If this set is found out to be unsatisfiable, the interpreter [[Backtracking|backtracks]], trying to use other clauses for proving the goal. In practice, satisfiability of the constraint store may be checked using an incomplete algorithm, which does not always detect inconsistency.
|