Group: formalism
Group: artificial intelligence
Topic: backtracking
Topic: constructing proof and program together
Topic: continuation
Topic: descriptive languages
Topic: lambda calculus
Topic: formal methods and languages
Topic: logic
Topic: mathematical proof
Topic: nondeterministic processing
Topic: production systems
Topic: problems with logic programming
Topic: symbolic execution
Topic: theorem proving systems
 
Summary
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. Forloops 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
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 nondeterministic 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 firstorder 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
Quote: resolution combines substitution with truthfunctional analysis; includes proof of completeness and discussion of efficient proofprocedures [»robiJA1_1965]
 Quote: resolution is an inference principle specifically designed for computer theoremproving 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 firstorder 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
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
Quote: bddbddb generates efficient, binary decision diagrams for stratified Datalog programs; e.g., contextsensitive pointer analysis, side effect analysis, type analysis, and escape analysis [»whalJ6_2004]
 Quote: use binary decision diagrams (BDD) for subsetbased pointsto analysis; BDDs from model checking; simple, less space, scales well [»bernM6_2003]
 Quote: store pointsto information as binary decision diagrams in bddbddb; from Whaley and Lam's pointer alias analysis; query with Datalog [»martM10_2005]
 Subtopic: security as logic
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
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
Quote: logical implication should be like a procedure, e.g., invoked by beliefs [»hewiC4_1985]
 Quote: Planner procedures can be goalinvoked, i.e., a subgoal is derived [»hewiC4_1985]
 Quote: Planner theorems are imperatives when executed and declaratives when data [»hewiC4_1985]
 Quote: in constraintoriented programming, a process is deduction from an initial state under sets of constraints and inputs [»nygaK10_1986]
 Subtopic: logical constraints
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
Quote: the relational model is as powerful as the firstorder predicate logic in retrieving information [»coddEF_1990]
 Subtopic: examples
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
QuoteRef: cbb_1973 ;;4/25/74 A program is a sequence of true statements that are made true eg a=b

Related Topics
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: nondeterministic 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)
