| |
 |
|
|
Gibert, Jacek
The University of Melbourne
Parkville, Australia
|
|
 |
|
|
| |
| |
|
Date Reviewed |
|
| |
1 - 10 of 14
reviews
|
|
|
|
|
|
|
|
Formal semantics for mutual belief
Colombetti M. Artificial Intelligence 62(2): 341-353, 1993. Type: Article
A concise mathematical description of semantics for mutual belief is provided. The author demonstrates that mutual belief can be naturally defined in terms of private beliefs within a traditional possible world semantics. In particular...
|
Aug 1 1994 |
|
|
|
|
|
|
The organization of reduction, data flow, and control flow systems
Kluge W., MIT Press, Cambridge, MA, 1992. Type: Book (9780262610810)
It is becoming increasingly evident that, to obtain more performance from computer architecture in the future, one must look beyond the time-honored von Neumann model of a computing system. Much ground-breaking theoretical work has bee...
|
Mar 1 1994 |
|
|
|
|
|
|
A proof theory for general unification
Snyder W., Birkhäuser Boston Inc., Cambridge, MA, 1991. Type: Book (9780817635930)
Almost every automated deduction system relies on unification in one form or another. Since the early 1960s, many implementations of unification have been produced in the field of automated deduction, from artificial intelligence to fo...
|
Mar 1 1993 |
|
|
|
|
|
|
Temporal predicate transforms and fair termination
Morris J. Acta Informatica 27(4): 287-313, 1990. Type: Article
Much of the literature on fair termination of nondeterministic programs has been concerned with formalizing this concept. Morris’s paper follows this trend but with some important differences....
|
Dec 1 1990 |
|
|
|
|
|
|
Communicating process architecture
, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988. Type: Book (9789780136293200)
This collection of INMOS technical notes is presented in two sections, “Principles” and “Practice,” which together form a good explanation of the architectural foundations of OCCAM and the INMOS ...
|
Oct 1 1990 |
|
|
|
|
|
|
BCK-combinators and linear &lgr;-terms have types
Hindley J. Theoretical Computer Science 64(1): 97-105, 1989. Type: Article
This short theoretical paper on lambda calculus investigates linear &lgr;-terms and the corresponding variable-free BCK-combinators....
|
Feb 1 1990 |
|
|
|
|
|
|
Deduction Graphs: An Algorithm and Applications
Yang C. IEEE Transactions on Software Engineering 15(1): 60-67, 1989. Type: Article
Yang proposes a new graphical method based on deduction graphs to solve dependency, rule, and fact inference problems in relational databases, rule-based expert systems, logic programming, and general AI. The paper presents an algorith...
|
Sep 1 1989 |
|
|
|
|
|
|
History and basic features of the critical-pair/completion procedure
Buchberger B. (ed) Journal of Symbolic Computation 3(1-2): 3-38, 1987. Type: Article
This paper is an excellent intuitive presentation of the critical pair/completion (CPC) techniques for solving algorithmic problems. It covers areas of CPC research and applications which range from automated theorem proving and rewrit...
|
May 1 1989 |
|
|
|
|
|
|
From logic design to logic programming: theorem proving techniques and P-functions
Snyers D., Thayse A. (ed), Springer-Verlag New York, Inc., New York, NY, 1987. Type: Book (9789780387182179)
The P-function calculus is an algebraic formalism for representing algorithms and synthesizing their implementations. This calculus was introduced and used in earlier published works by one of the authors [for example, see 1]. ...
|
Jun 1 1988 |
|
|
|
|
|
|
Soundness of Hoare’s logic: an automated proof using LCF
Sokolowski S. ACM Transactions on Programming Languages and Systems 9(1): 100-121, 1987. Type: Article
The paper gives a lively account of the “ups and downs” during an experiment with the Edinburgh LCF theorem prover. The author relaxes the concrete syntax of LCF and skips cumbersome technical details, making this p...
|
Dec 1 1987 |
|
|
|
|
|
| |
|
|
| |
|
|
