Topic: logic programming

topics > computer science > programming > Group: types of programming languages


artificial intelligence
constructing proof and program together
descriptive languages
lambda calculus
formal methods and languages
mathematical proof
non-deterministic processing
production systems
problems with logic programming
symbolic execution
theorem proving systems


A program can be seen as a series of logical statements. The processor's job is 'proving' each statement by transforming values. Input is statement modifiers (e.g., 'where x=3') while output is the set of values making all statements true (e.g. with the above modifier, the statement 'x = y - 5' would output 8 for y). Computation becomes a sequence of goal statements incrementally derived. The sequence, though critical for program efficiency, is indeterminate. For-loops are represented by the universal quantifier.

Advantages-- A close match to predicate logic allows the results and theorems of predicate logic to be transferred directly to programming methodology. (cbb 5/80)

Subtopic: logic programming up

Quote: a computation in logic programming consists of a sequence of goal statements derived from a set of Horn clauses [»kowaR11_1973]
Quote: an inference principle needs to be sound (i.e., allow only logical consequences) and effective (i.e., algorithmically decidable)
Quote: logic programming is non-deterministic since a procedure call matches more than one definition [»kowaR11_1973, OK]
Quote: Horn clauses have a single antecedent; define procedures, assert facts, and specify goals [»kowaR11_1973, OK]
Quote: implication in first-order logic can be replaced by unsatisfiability of sentences in clausal form [»kowaR11_1973]
Quote: an atomic formula in a logic clause is a predicate over variables and functions of variables or functions of functions...
QuoteRef: kowaR11_1973 ;;5 Clausal definition of factorial: (F1) fact (0,1)<- (F2) Fact (x+1,u) <- Fact (x,v), Times (x+1, v, u) (F3) <- Fact (2,y) here y=2 (the solution) contradicts F1 and F2 since Fact (0,v) and Times (2, v, u) is true if v=1 (from Fact (0,1) and u=2 since Times (2,1,2)

Subtopic: resolution up

Quote: resolution combines substitution with truth-functional analysis; includes proof of completeness and discussion of efficient proof-procedures [»robiJA1_1965]
Quote: resolution is an inference principle specifically designed for computer theorem-proving programs; the complexity of the principle does not matter; permits a very compact, not to say elegant, piece of reasoning [»robiJA1_1965]
Quote: resolution may be the first complete system of first-order logic using just one inference principle [»robiJA1_1965]
Quote: the resolution principle -- from any two clauses, one may infer a resolvent; a refutation is a sequence of resolutions leading to the empty clause; unsatisfiable iff refutation [»robiJA1_1965]
Quote: resolution search principles include purity (one may delete pure clauses), subsumption (C subsumes D if there is a substitution), and replacement (a resolvent may replace a subsumed clause) [»robiJA1_1965]
Quote: can create a useful inference system from only resolution; like, matching procedure definitions to procedure calls [»kowaR11_1973]
Quote: if terms are written as their indefinable, first terms, it is easy to resolve predicates and derive terms [»leibGW_1666]

Subtopic: temporal logic up

Quote: SPIN represents correctness claims in linear temporal logic (LTL)
Quote: the TimeLine graphical editor simplifies the specification of basic temporal properties for SPIN model checkers; linear temporal logic is difficult to use [»holzGJ11_2002]

Subtopic: stratified programs, binary decision diagram up

Quote: bddbddb generates efficient, binary decision diagrams for stratified Datalog programs; e.g., context-sensitive pointer analysis, side effect analysis, type analysis, and escape analysis [»whalJ6_2004]
Quote: use binary decision diagrams (BDD) for subset-based points-to analysis; BDDs from model checking; simple, less space, scales well [»bernM6_2003]
Quote: store points-to information as binary decision diagrams in bddbddb; from Whaley and Lam's pointer alias analysis; query with Datalog [»martM10_2005]

Subtopic: security as logic up

Quote: SD3 extends datalog by associating names with authenticated public keys, e.g., T(x,y):-K$E(x,y) holds if E(x,y) and relation E under keyholder of K [»jimT5_2000]
Quote: secure DNS resolver in 10 lines of code; easier to understand than BIND's security policy [»jimT5_2000]

Subtopic: Prolog up

Quote: in Prolog the specification is the implementation [»warrDH2_1980]
Quote: Prolog executes a goal by finding a clause with a matching head and then executing its goals left to right; Prolog backtracks on failure [»warrDH2_1980]
Quote: one Prolog rule can define several functions, e.g., append defines concatenation, a test, and two completions [»tichWF11_1987]

Subtopic: logical implication up

Quote: logical implication should be like a procedure, e.g., invoked by beliefs [»hewiC4_1985]
Quote: Planner procedures can be goal-invoked, i.e., a sub-goal is derived [»hewiC4_1985]
Quote: Planner theorems are imperatives when executed and declaratives when data [»hewiC4_1985]
Quote: in constraint-oriented programming, a process is deduction from an initial state under sets of constraints and inputs [»nygaK10_1986]

Subtopic: logical constraints up

Quote: data and procedure by primitive constraints: an object with parts for data fields/parameters and a body of rules in an implementation language [»deutLP1_1981]
Quote: example of addition constraint showing how given any two parts can compute the third part [»deutLP1_1981]
Quote: in a constraint, if insufficient information to run a rule then ignore; if inconsistent information, then fail [»deutLP1_1981]

Subtopic: relational model up

Quote: the relational model is as powerful as the first-order predicate logic in retrieving information [»coddEF_1990]

Subtopic: examples up

QuoteRef: hallJC5_1974 ;;41 alternation by d=b : b if a succeeds save cursor and needle follow d's subsequent. If this fails then backtrack to b

Subtopic: program and logic up

QuoteRef: cbb_1973 ;;4/25/74 A program is a sequence of true statements-- that are made true eg a=b

Related Topics up

Group: formalism   (9 topics, 478 quotes)

Group: artificial intelligence   (14 topics, 509 quotes)
Topic: backtracking (30 items)
Topic: constructing proof and program together (22 items)
Topic: continuation (16 items)
Topic: descriptive languages (22 items)
Topic: lambda calculus (16 items)
Topic: formal methods and languages (53 items)
Topic: logic (84 items)
Topic: mathematical proof (23 items)
Topic: non-deterministic processing (19 items)
Topic: production systems (10 items)
Topic: problems with logic programming (10 items)
Topic: symbolic execution (9 items)
Topic: theorem proving systems
(20 items)

Updated barberCB 8/04
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.