Baroque(ID:576/bar001)

Logic programming language 

Boyer & Moore, Edinburgh, 1972.

Logic programming language with non-logic programming features

Kowalski:
"assembly-like programming language that provided list processing and arithmetic primitives defined by Horn clauses and interpreted by a structure- sharing SL-resolution theorem prover with a depth-first search strategy"


Places
References:
  • Bayer, R.S., and Moore, JS. "The sharing of structure in theorem proving programs" pp101-116 view details
          in "Machine Intelligence 7", Meltzer, Bernard and Michie, Donald (eds) Edinburgh University Press, 1972 view details
  • Moore, J S. "Computational logic: Structure sharing and proof of program properties" Ph D. Department of Computational Logic, School of Artif Intel., U. of Edinburgh, Edinburgh, 1973. view details
          in "Machine Intelligence 7", Meltzer, Bernard and Michie, Donald (eds) Edinburgh University Press, 1972 view details
  • Moore, J. "Computational logic: Structure sharing and proof of program properties, Parts I and II" Department of Computational Logic Memo 67, School of Artificial Intelligence, Univ. of Edinburgh, Edinburgh, U.K., 1974. view details
          in "Machine Intelligence 7", Meltzer, Bernard and Michie, Donald (eds) Edinburgh University Press, 1972 view details
  • Boyer. R.S.. and Moore, JS. "Proving theorems about LISP functions" pp129-144 view details Abstract: Program verification is the 1den that propertms of programs can be precisely stated and proved in the mathematical sense. In this paper, some simple heuristics combimng evaluation and mathematical reduction are described, which the authors have implemented in a program that automatically proves a wide varietyof theorems about recursive Lisp functions. The method the program uses to generate induction formulas is described at length The theorems proved by the program include that REVERSE is its own inverse and that a particular SORT program is correct. A list of theorems proved by the program is given DOI
          in [ACM] JACM 22(1) January 1975 view details
  • Kowalski, Robert A. "The early years of logic programming" pp38-43 view details Abstract: This firsthand recollection of those early days of logic programming traces the shared influences and inspirations that connected Edinburgh, Scotland, and Marseilles, France. Extract: Kowalski on Baroque
    When I returned from Marseilles, Boyer and Moore were very enthusiastic. Programming in resolution logic seemed to be just what they were looking for to exploit their earlier discovery of the structure sharing method of implementing resolution. They were already aware that structure sharing was analogous to the use of association lists in the implementation of Lisp. By the summer of 1972, however, they were so enthusiastic that they developed their own logic programming language called Baroque [27].

    Baroque was an assembly-like programming language that provided list processing and arithmetic primitives defined by Horn clauses and interpreted by a structure- sharing SL-resolution theorem prover with a depth-first search strategy. "Demons" were attached to primitive functions such as addition and multiplication, to exploit the machine’s built-in arithmetic. Boyer and Moore then coded an interpreter in Baroque for a programming language akin to pure Lisp, with pattern- matched invocation and nondeterminism inherited from its implementation language. Programs written in the Lisp-like language were about 10 times slower than similar programs written directly in Baroque. However, what intrigued Boyer and Moore about the language was that it permitted (indeed, encouraged) the symbolic execution of programs and hence the interpreter could prove simple theorems about programs, such as "There exists an X such that (Length X) is 3." As they tried to prove more complicated theorems about programs, for example, that append is associative or that the length of (Append A B) is the sum of the lengths of A and B, they realized it was necessary to do mathematical induction. Boyer and Moore then turned their attention toward mechanizing inductive proofs.


          in [ACM] CACM 31(01) (Jan 1988). view details