E1AR0002@SMUVM1.BITNET (06/04/86)
%A John W. Lloyd %A Rodney W. Topor %T Making Prolog More Expressive %R Technical Report 84/8 %I Department of Computer Science, University of Melbourne %D June 1984 %P 22 %K first order logic, programming in logic, deductive databases, query language AI10 AA14 AA09 %O also in Journal of Logic Programming, vol.4, 1984 %X This paper introduces extended programs and extended goals for logic programming. A clause in an extended program can have an arbitrary first order formula as its body. Similarly, an extended goal can have an arbitrary first order formula as its body. The main results of the paper are the soundness of the negation as failure rule and SLDNF-resolution for extended programs and goals. We show how the increased expressibility of extended programs and goals can be easily implemented in any PROLOG system which has a sound implementation of the negation as failure rule. We also show how these ideas can be used to implement first order logic as a query language in a deductive database system. An application to integrity constraints in deductive database systems is also given. %A Jacek Gibert %T J-Machine User's Manual %R Technical Report 84/10 %I Department of Computer Science, University of Melbourne %D November 1984 %P 42 %K functional programming, graph reduction machines, combinators H03 %X This manual describes an experimental software implementation of a combinatory reduction machine called the J-Machine. The J-Machine is mainly oriented towards symbol manipulation and it aims at exposing flows of data, and a high degree of parallelism in ordinary functional programs. It executes directly the J'' reduction language which is based upon a variant of the full combinatory theory. The J'' language has an associated algebra of functions which allows a user to prove properties of functional programs with the assistance of the J-Machine. With the advent of hardware concepts like data driven reduction architectures, VLSI implementation of the J-Machine appears to be an attractive proposition. But at the present, the J-Machine is an interactive interpreter written in the C programming language under the Unix operating system. %A Lee Naish %T Prolog Control Rules %R Technical Report 84/13 %I Department of Computer Science, University of Melbourne %D September 1984 %P 12 %K AI10 computational rules %O a shortened version appeared in Proceedings of the International Joint Conference on Artificial Intelligence, Los Angeles, 1985 %A Joxan Jaffar %A Jean-Louis Lassez %A Michael J. Maher %T A Logic Programming Language Scheme %R Technical Report 84/15 %I Department of Computer Science, University of Melbourne %D November 1984 %P 22 %K theory, semantics AI10 T02 %O also appeared in Logic Programming: Relations, Functions and Equations'', D.DeGroot and G.Lindstrom (eds.), Prentice-Hall, 1985 %X Numerous extended versions of PROLOG are now emerging. Im order to provide greater versatility and expressive power, some versions allow functional programming features, others allow infinite data structures. However, there is concern that such languages may have little connection left with logic. In some instances, various logical frameworks have been proposed to solve this problem. Nevertheless, the crucial point has not been addressed: the preservation of the unique semantic properties of logic programs. The significance of our effort here is twofold: (1) There is a natural logic programming language scheme wherein these properties hold. (2) Formal foundations for extended versions of traditional PROLOG can be obtained as instances of this scheme. They automatically enjoy its properties. %A T. Y. Chen %A Jean-Louis Lassez %A Graeme S. Port %T Maximal Unifiable Subsets and Minimal Non-unifiable Subsets %R Technical Report 84/16 %I Department of Computer Science, University of Melbourne %D November 1984 %P 20 %K unification, backtracking, resolution AI11 %A John W. Lloyd %A Rodney W. Topor %T A Basis for Deductive Database Systems %R Technical Report 85/1 %I Department of Computer Science, University of Melbourne %D February 1985 (revised April 1985) %P 22 %K logic programming, first order logic, soundness, integrity constraints AA14 AA09 T02 %X This paper provides a theoretical basis for deductive database systems. A deductive database consists of closed typed first order logic formulas of the form A<-W, where A is an atom and W is a typed first order formula. A typed first order formula can be used as a query and a closed typed first order formula can be used as an integrity constraint. Functions are allowed to appear in formulas. Such a deductive database system can be implemented using a PROLOG system. The main results are the soundness of the query evaluation process, the soundness of the implementation of integrity constraints, and a simplification theorem for implementing integrity constraints. A short list of open problems is also presented. %A Richard A. Helm %A Catherine Lassez %A Kimball G. Marriott %T Prolog for Expert Systems: An Evaluation %R Technical Report 85/3 %I Department of Computer Science, University of Melbourne %D June 1985 %P 20 %K TEAS, MARLOWE, knowledge representation AI01 T02 %O also in Proceedings of Expert Systems in Government'', Virginia, 1985 %A John W. Lloyd %A Rodney W. Topor %T A Basis for Deductive Database Systems II %R Technical Report 85/6 %I Department of Computer Science, University of Melbourne %D February 1985 (revised April 1985) %P 17 %K AI10 first order logic, soundness, integrity constraints, query evaluation AA09 AA14 %X This paper is the third in a series providing a theoretical basis for deductive database systems. A deductive database consists of closed typed first order logic formulas of the form A<-W, where A is an atom and W is a typed first order formula. A typed first order formula can be used as a query and a closed typed first order formula can be used as an integrity constraint. Functions are allowed to appear in formulas. Such a deductive database system can be implemented using a PROLOG system. The main results of this paper are concerned with the non-floundering and completeness of query evaluation. We also introduce an alternative query evaluation process and show that corresponding versions of the earlier results can be obtained. Finally, we summarize the results of the three papers and discuss the attractive properties of the deductive database system approach based on first order logic. %A Lee Naish %T The MU-Prolog 3.2 Reference Manual %R Technical Report 85/11 %I Department of Computer Science, University of Melbourne %D October 1985 %P 17 %K AI10 T02 %X MU-PROLOG is (almost) upward compatible with DEC-10 PROLOG, C-PROLOG and (PDP-11) UNIX PROLOG. The syntax and built-in predicates are therefore very similar. A small number of DEC-10 predicates are not available and some have slightly different effects. There are also some MU-PROLOG predicates which are not defined in DEC-10 PROLOG. However most DEC-10 programs should run with few, if any, alterations. However, MU-PROLOG is not intended to be a UNIX PROLOG look-alike. MU-PROLOG programs should be written in a more declarative style. The non-logical predicates'' such as cut (!), \\=, not and var are rarely needed and should be avoided. Instead, the soundly implemented not (~), not equals (~=) and if-then-else should be used and wait declarations should be added where they can increase efficiency. This is a reference manual only, not a guide to writing PROLOG programs. %A Lee Naish %T Negation and Control in PROLOG %R Technical Report 85/12 %I Department of Computer Science, University of Melbourne %D September 1985 %P 108 %K T02 resolution, PhD thesis %X We investigate ways of bringing PROLOG closer to the ideals of logic programming, by improving its facilities for negation and control. The forms of negation available in conventional PROLOG systems are implemented unsoundly, and can lead to incorrect solutions. We discuss several ways in which negation as failure can be implemented soundly. The main forms of negation considered are not'', not-equals'', if-then-else'' and all solutions predicates. The specification and implementation of all solutions predicates is examined in detail. Allowing quantifiers in negated calls is an extension which is easily implemented and we stress its desirability, for all forms of negation. We propose other enhancements to current implementations, to prevent the computation aborting or looping infinitely, and also outline a new technique for implementing negation by program transformation. Finally, we suggest what forms of negation should be implemented in future PROLOG systems. %A Lee Naish %T Negation and Quantifiers in NU-Prolog %R Technical Report 85/13 %I Department of Computer Science, University of Melbourne %D October 1985 %P 12 %K T02 control %X We briefly discuss the shortcomings of negation in conventional Prolog systems. The design and implementation of the negation constructs in NU-Prolog are then presented. The major difference is the presence of explicit quantifiers. However, several other innovations are used to extract the maximum flexibility from current implementation techniques. These result in improved treatment of \*(lqif\*(rq, existential quantifiers, inequality and non-logical primitives. We also discuss how the negation primitives of NU-Prolog can be added to conventional systems, and how they can improve the implementation of higher level constructs. %A Michael J. Maher %T Semantics of Logic Programs %R Technical Report 85/14 %I Department of Computer Science, University of Melbourne %D September 1985 %P 77 %K logic programming theory, fixed points, fixedpoints, PhD thesis AI10 %X This thesis deals with the semantics of definite clause logic programs in the presence of an equality theory. Definite clauses are the formal foundation of the PROLOG programming language. Definitions of functions and abstract data types use equality. Many have suggested the incorporation of these features into a logic programming language and already there are many of these languages. This thesis provides a formal foundation for such languages. The treatment consistently factors out the equality theory to obtain the effect of a scheme: any equality theory which satisfies some appropriate conditions can be used as part of the programming language. %A Philip W. Dart %A Justin A. Zobel %T Conceptual Schemas Applied to Deductive Databases %R Technical Report 85/16 %I Department of Computer Science, University of Melbourne %D November 1985 %P 29 %K prolog, query language, graphical interface, conceptual schema, deductive database AI10 %X Much of the information required in the formulation of a query is inherent in the database structure. First order logic is a powerful query language, but does not exploit this structure or provide an accessible interface for naive users. A new conceptual schema formalism, based directly on logic, provides the necessary description of the database structure. Its graphical representation is the basis for a simple, concise graphical query language with the expressive power of first order logic. %A Kotagiri Ramamohanarao %A John A. Shepherd %T A Superimposed Codeword Indexing Scheme for Very Large Prolog Databases %R Technical Report 85/17 %I Department of Computer Science, University of Melbourne %D November 1985 %P 20 %K partial match retrieval, Prolog, hashing, descriptors, optimization T02 AA09 %X This paper describes a database indexing scheme, based on the method of superimposed codewords, which is suitable for dealing with very large databases of Prolog clauses. Superimposed codeword schemes provide a very efficient method of retrieving records from large databases in only a small number of disk accesses. This system supports the storage and retrieval of general Prolog terms, including functors and variables, and it is possible to store Prolog rules in the database. %A James A. Thom %A Kotagiri Ramamohanarao %A Lee Naish %T A Superjoin Algorithm for Deductive Databases %R Technical Report 86/1 %I Department of Computer Science, University of Melbourne %D February 1986 %P 10 %K partial match retrieval, prolog, hashing, joins, optimization, database relational, deductive AI10 AA09 %X This paper describes a join algorithm suitable for deductive and also relational databases which are accessed by computers with large main memories. Using multi-key hashing and appropriate buffering, joins can be performed on very large relations more efficiently than with existing methods. Furthermore, this algorithm fits naturally into a Prolog top-down computation and can be made very flexible by incorporating additional Prolog features. %A Lee Naish %T Don't Care Nondeterminism in Logic Programming %R Technical Report 86/? %I Department of Computer Science, University of Melbourne %D February 1986 %P 10 %K indeterminism, incompleteness, cut, commit, trust, parallel, proving AI10 %X Prolog and its variants are based on SLD resolution, which uses don't know nondeterminism to explore the search space. Don't care nondeterminism, or indeterminism, can be introduced by operations such as commit in Concurrent Prolog, cut in sequential Prolog and incomplete system predicates. This prevents the whole SLD tree from being examined. The effect on completeness of programs is of major importance. This paper presents a theoretical model of \fIGuarded Clauses\fP, which subsumes the main features of sequential and concurrent Prologs. Next, we investigate proving properties of Guarded Clause programs with restricted input-output modes. We present a methodology for proving that the indeterminism does not cause finite failure, given certain input conditions. %A John W. Lloyd %T Declarative Error Diagnosis %R Technical Report 86/? %I Department of Computer Science, University of Melbourne %D February 1986 %P 20 %K algorithmic debugging, logic programming AI10 T02 O02 AI01 %X This paper presents an error diagnoser which finds errors in extended logic programs and also logic programs which use advanced control facilities. The diagnoser is declarative'', in the sense that the programmer need only know the intended interpretation of an incorrect program to use the diagnoser. In particular, the programmer needs no understanding whatever of the underlying computational behaviour of the PROLOG system which runs the program. It is argued that declarative error diagnosers will be indispensable components of advanced logic programming systems, which are currently under development. %A J. Heering %T Partial Evaluation and W-Completeness of Algebraic Specifications %D 1985 %R Report CS-R8501 %I Centre for Mathematics and Computer Science %C Amsterdam, The Netherlands %K AA08 %X f 3,90 14 pages %A J. C. M. Baeten %A J. A. Bergstra %A J. W. Klop %T Conditional axioms and $alpha beta$ calculus in process algebra %D 1985 %R Report CS-R8502 %I Centre for Mathematics and Computer Science %C Amsterdam, The Netherlands %K AA08 %X f 3,90 26 pages %A J. C. M. Baeten %A J. A. Bergstra %A J. W. Klop %T Syntax and Defining Equations for an Interupt Mechanism in Process Algebra %D 1985 %R Report CS-R8503 %I Centre for Mathematics and Computer Science %C Amsterdam, The Netherlands %K AA08 %X f 7,60 45 p %A J. W. de\0Bakker %T Transition Systems, Infinitary Languages and the Semantics of Uniform Concurrency %D 1985 %R Report CS-R8506 %I Centre for Mathematics and Computer Science %C Amsterdam, The Netherlands %K AA08 %X f 3,90 11 pages %A J. Heering %A P. Klint %T The Efficiency of the Equation Interpreter Compared with the UNH PROLOG Interpreter %D 1985 %R Report CS-R8509 %I Centre for Mathematics and Computer Science %C Amsterdam, The Netherlands %K T02 AI10 %X f 3,90 13 pages %A M. L. Kersten %A H. Weigand %A F. Dignum %T A Conceptual Modeling Expert System %D 1985 %R Report CS-R8518 %I Centre for Mathematics and Computer Science %C Amsterdam, The Netherlands %K AI01 %X f 3,90 14 pages %A N. W. P. van\ Diepen %A W. P. de\ Roever %T Program Derivation Through Transformations: the Evolution of List-Copying Algorithms %D 1985 %R Report CS-R8520 %I Centre for Mathematics and Computer Science %C Amsterdam, The Netherlands %K AA08 %X f 8,80 60 pages %A Bertrand Meyer %T The Software Knowledge Base %R TRCS85-04 %I University of California, Santa Barbara %K AA08 %A Bernard Nadel %T The General Consistent Labeling (or Constraint Satisfaction) Problem %R CRL-TR-2-86 %I University of Michigan Computing Research Laboratory %K AI03 %A William G. Golson %T A Complete Proof System for an Acceptance Refusal Model of CSP %R TR85-19 %I Rice University Department of Computer Science %K AA08 %A Raghu Ramakrishman %A Avi Silberschatz %T Annotations for Distributed Programming in Logic %R TR-85-15 %D SEP 1985 %I University of Texas at Austin Department of Computer Sciences %K H03 T02 AI10 %A E. Allen Emerson %A Chin-Laung Lei %T Branching Time Logic Strikes Back %R TR-85-21 %D OCT 1985 %I University of Texas at Austin Department of Computer Sciences %K temporal logic finite automata infinite strings AA08 AI11 %A Christian Lengauer %A Chua-Huang Huang %T A Mechanically Certified theorem about Optimal Concurrency of Sorting Networks %R TR-85-23 %D OCT 1985 %I University of Texas at Austin Department of Computer Sciences %K H03 AI11 AA08 %A A. Udaya Shankar %A Simon S. Lam %T Time-Dependent Distributed Systems: Proving Safety, Liveness and Real-Time Properties %R TR-85-24 %D OCT 1985 %I University of Texas at Austin Department of Computer Sciences %K H03 AI11 A08 %X includes information on verification of communication protocols including HDLC and a transport-layer protocol of window size N %A E. Allen Emerson %A A. Prasad Sistla %T Deciding Full Branching Time Logic %R TR-85-28 %D NOV 1985 %I University of Texas at Austin Department of Computer Sciences %K AI10a %A E. Allan Emerson %A Joseph Y. Halpern %T Decision Procedures and Expressiveness in the Temporal Logic of Branching Time %R TR-85-29 %D NOV 1985 %I University of Texas at Austin Department of Computer Sciences %K AI10a %A E. M. Clarke %A E. A. Emerson %A A. P. Sistla %T Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications %R TR-85-31 %D NOV 1985 %I University of Texas at Austin Department of Computer Sciences %K AI10a H03 AA08 %A Benjamin Kuipers %T The Map-Learning Critter %R TR-85-33 %D DEC 1985 %I University of Texas at Austin Department of Computer Sciences %K AI07 AI04 %X "The Critter is an artificial creature which learns, not only the structure of its (simulated) environment, but also the interpretation of the actions and senses that give it access to that environment." %A Newton S. Lee %A John W. Roach %T Guess/1: A General Purpose Expert Systems Shell %R 85-3 %I Virginia Tech Computer Science Department %K T03 %A John W. Roach %A Glenn Fowler %T Virginia Tech Prolog/Lisp A Dual Interpeter Implementation %R 85-18 %I Virginia Tech Computer Science Department %K T01 T02 %A J. Patrick Bizler %A Layne T. Watson %A J. Patrick Sanford %T Spline Based Recognition of Straight Lines and Curves in Engineering Line Drawing %R 85-29 %I Virginia Tech Computer Science Department %K AI06 AA05 %A Richard E. Nance %A Robert L. Moose %A Robert V. Foutz %T A Statistical Technique for Comparing Strategies: An Example from Computer Network Design %R 85-26 %I Virginia Tech Computer Science Department %K O04 AA08 AI09 anova %A T. C. Hu %A M. T. Shing %T The Alpha-Beta Routing %R TRCS85-08 %I University of California, Santa Barbara %K AA05