Content deleted Content added
Cybercobra (talk | contribs) +infobox |
lk automated theorem proving, rm Metamath (not relevant) |
||
Line 80:
== History ==
The first application of IPL was to demonstrate that the theorems in ''[[Principia Mathematica]]'' which were laboriously proven by hand, by [[Bertrand Russell]] and [[Alfred North Whitehead]], could in fact be [[automated theorem proving|proven by computation]]. According to Simon's autobiography ''Models of My Life'', this first application was developed first by hand simulation, using his children as the computing elements, while writing on and holding up note cards as the registers which contained the state variables of the program.▼
▲The first application of IPL was to demonstrate that the theorems in ''[[Principia Mathematica]]'' which were laboriously proven by hand, by [[Bertrand Russell]] and [[Alfred North Whitehead]], could in fact be proven by computation. According to Simon's autobiography ''Models of My Life'', this first application was developed first by hand simulation, using his children as the computing elements, while writing on and holding up note cards as the registers which contained the state variables of the program.
IPL was used to implement several early [[artificial intelligence]] programs, also by the same authors: the [[Logic Theory Machine]] (1956), the [[General Problem Solver]] (1957), and their [[computer chess]] program [[NSS (chess program)|NSS]] (1958).
Line 90 ⟶ 89:
== Legacy to computer programming ==
IPL arguably introduced several programming language features:
* '''List manipulation''' (but only lists of atoms, not general lists)
Line 113 ⟶ 111:
* [http://bitsavers.org/pdf/rand/ipl/] IPL documents from BitSavers.
* [http://www-formal.stanford.edu/jmc/history/lisp/node2.html] influence of IPL on LISP.
[[Category:Procedural programming languages]]
| |||