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:
non-deterministic 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. 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 
| 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
| 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
| 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., 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
| 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 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
| 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 first-order 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: 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)
|
