|
 ABSTRACT
Exactly 100 years ago, the first-order predicate calculus was created and defined by Gottlob Frege. In the ensuing century his system was studied and refined by such logicians as Bertrand Russell, David Hilbert, Kurt Godel, Jacques Herbrand, Alonzo Church, and Alan Turing. In the 1950's and 60's attempts were made to use the results of these studies (especially those of Herbrand) in order to program computers to prove theorems automatically. These attempts introduced a new demon to the study of logic: ferocious computational complexity. The investigations of methods to avoid this demon led to the development of new systems of logic which are equivalent to the traditional systems, but are more suited to the efficient mechanical construction of proofs. The most notable among these is the resolution system of J. Alan Robinson [1965],[1979]. Cordell Green [1969] proposed the use of resolution systems in the construction of deductive question-answering systems, and this proposal eventually led Robert Kowalski [1974] to propose the so-called procedural interpretation of logic which forms the basis for the use of logic as a programming language.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
 |
1
|
|
| |
2
|
Clark, Keith {1978} Negation as failure, in Logic and Data Bases, H. Gallaire and J. Minker (eds.), New York: Plenum Press, 293-322.
|
| |
3
|
Clark, Keith L. and van Emden, Maarten H. {1979} Consequence verification of flowcharts, Report CS-79-23, Department of Computer Science, University of Waterloo, Waterloo, Ontario, Canada.
|
| |
4
|
Clark, Keith L. and McCabe, Frank {1979} IC-PROLOG, Proc. AISB.
|
| |
5
|
Clark, Keith L. and Tarnlund, Sten-ake {1977} A First-order theory of data and programs, in Information Processing 77, B. Gilchrist (ed.), Amsterdam, North Holland, 939-944.
|
| |
6
|
|
| |
7
|
|
| |
8
|
Colmerauer, A., Kanoui, H., Pasero, R., Roussel, P. {1973} Un Systeme de Comunication Homme-machine en Francaies. Rapport Groupe d'Intelligence Artificielle, Universite d'Aix-Marseille, Luminy.
|
| |
9
|
|
| |
10
|
Maarten H. van Emden {1976} Verification conditions as programs, in Automata, Languages, and Programming, S. Michaelson and R. Milner (eds.), Edinburgh: Edinburgh University Press.
|
| |
11
|
Programming in resolution logic, in Machine Intelligence 8, E.W. Elcock and D. Michie (eds.), Edinburgh: Edinburgh University Press.
|
| |
12
|
Computation and Deductive Information Retrieval, in Formal Descriptions of programming Concepts, E.J. Neuhold (ed.), Amsterdam: North Holland.
|
| |
13
|
|
| |
14
|
van Emden, Maarten H. and de Lucena, G.J. {1979} Predicate logic as a language for parallel programming, Faculty of Mathematics Report CS-79-15, University of Waterloo.
|
| |
15
|
Green, Cordell {1969} Theorem-proving by resolution as a basis for question answering systems, in Machine Intelligence 4, B. Meltzer and D. Michie (eds.), Edinburgh: Edinburgh University Press.
|
| |
16
|
|
| |
17
|
Hill, Robert {1974} LUSH-resolution and its completeness, DCL Memo 78, Department of Computational Logic, University of Edinburgh.
|
| |
18
|
Kowalski, Robert {1974} Predicate logic as a programming language, Proc. IFIP 74, Amsterdam: North Holland, 556-574.
|
| |
19
|
Logic for data description, in Logic and Data Bases, H. Gallaire and J. Minker (eds.), New York: Plenum Press, 77 103.
|
| |
20
|
|
| |
21
|
Kowalski, Robert, and Kuehner, Donald {1971} Linear resolution with selection function, Artificial Intelligence 2, 227-260.
|
| |
22
|
Kellog, Charles, Klahr, Philip, and Travis, Larry {1978} Deductive planning and pathfinding for relational data bases, in Logic and Data Bases, H. Gallaire and J. Minker (eds.), New York: Plenum Press, 179 - 200.
|
| |
23
|
Montague, Richard {1970} English as a formal language, in Linguaggi nella Societa e nella Tecnica, B. Visentini et al. (eds.), Milan: Edizioni di Comunita, 189 - 224; reprinted in: Formal Philosophy, Selected Papers of Richard Montague, R.H. Thomason (ed.), New Haven: Yale University Press, 1974, pp. 188 - 221.
|
| |
24
|
Minker, Jack {1978} An experimental relational data base system based on logic, in Logic and Data Bases, H. Gallaire and J. Minker (eds.), New York: Plenum Press, 107 -147.
|
| |
25
|
|
| |
26
|
Reiter, Raymond {1978} Deductive question-answering on relational data bases, in Logic and Data Bases, H. Gallaire and J. Minker (eds.), New York: Plenum Press, 149 - 177.
|
| |
27
|
Roberts, Grant M. {1977} An implementation of PROLOG, M.Sc. Thesis, Dept. of Computer Science, University of Waterloo.
|
| |
28
|
Roussel, P. {1975} PROLOG: Manuel e Reference et d'Utilisation. *Groupe d'Intelligence Artificielle, U.E.R. de Luminy, Universite d'Aix-Marseille.
|
| |
29
|
|
| |
30
|
{1979}Logic: Form and Function, Edinburgh: Edinburgh University Press.
|
| |
31
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.3