%A Zohar Manna %A Richard Waldinger %T The Origin of the Binary Search Paradigm %R STAN-CS-85-1044 %I Department of Computer Science, Stanford University %D March 1985 %X $2.75 - shows how binary search based algorithms in numerical analysis would be derived by an automatic program-synthesis system %A Anne von der Leith Gardner %T An Artificial Intelligence Approach to Legal Reasoning %R STAN-CS-85-1045 %I Department of Computer Science, Stanford University %D June 1984 %P 205 %X microfiche only $2.00 %A Jeffrey D. Ullman %A Allen Van Gelder %T Testing Applicability of Top-Down Capture Rules %R STAN-CS-85-1046 %I Department of Computer Science, Stanford University %D April 1985 %X $2.50 We extend the theory of "Capture rules", introduced in Ullman (1984) and Sagiv and Ullman (1984), as a way to plan the evaluation of queries in a "knowledge base." The central issue of the paper is how to adorn the nodes of a rule/goal graph with limited amounts of information that can be used to test wehtehr one can answer a query "top-down" as a Prolog would. Moreover, the test must be performed quickly, preferably in time that is polynomial in the size of hte logical rules in the "knowledge base." We define the "uniqueness" property for rules and give an efficient algorithms to generate a set of equalities among the sizes of arguments in sets of such rules. Satisfaction of these inequalities is sufficient for the top-down processing of rules to cnverge. We then give an efficient test for satisfaction of these inequalities. There is, of course, no polynomial test that is both necessary and sufficient for applicability of this or most any interesting capture rule. %A Zohar Manna %A Richard Waldinger %T Special Relations in Automated Deduction %R STAN-CS-85-1051 %I Department of Computer Science, Stanford University %D May 1985 %K relation replacement rule relation matching rule polarity %X $4.00 %A Ramsey W. Haddad %A Donald E. Knuth %T A programming and problem-solving seminar %R STAN-CS-85-1055 %I Department of Computer Science, Stanford University %D 1985 %P 103 %K CS204, Code breaking, Distributed stability, Hardware fault detection, High-tech art, Monotonic squares %X This report contains edited transcripts of the discussions held in Stanford's course, CS204, Problem Seminar, during Winter Quarter 1985." %A Martin Abadi %A Zohar Manna %T Nonclausal Temporal Deduction %R STAN-CS-85-1056 %I Department of Computer Science, Stanford University %D June 1985 %P 17 %K Nonclausal resolution, Propositional temporal logic, Theorem proving %X 2.75 %A Ian A. Mason %A Carolyn L. Talcott %T Memories of S-expressions: proving properties of Lisp-like programs that destructively alter memory %R STAN-CS-85-1057 %I Department of Computer Science, Stanford University %D June 1985 %P 46 %K Computations over memory structures, Correctness proofs, Robson copying algorithm %X $3.50