|
Artificial Intelligence, as a field of research, was basically created by a man
named John McCarthy, who came up with the name and convened the first academic
workshop on the subject (in Dartmouth, in 1956). John McCarthy (who is also
known as the creator of Lisp) was the student of Alonzo Church, who gave his
name to the Church-Turing Thesis and is remembered for his description of the
Lambda calculus, a model of computation equivalent to universal Turing machines.
These are all logicians, btw, mathematicians steeped in the work of the founders
of the field of mathematical logic as it was developed mainly in the 1920's by
Frege, Hillbert, Gödel, Russel and Whitehead, and others (of course there was
much work done before the 1920's, e.g. by Boole, Leibnitz... Aristotle... but it
only really got properly systematised in the 1920's). So it makes sense that the field of AI was closely tied with logic, for a long
time: because its founder was a logician. There were different strains of research in subjects and with goals adjacent to
and overlapping with AI, as John McCarthy laid them down. For example,
statistical pattern recognition or cybernetics (the latter intuition I owe to a
comment by Carl Hewitt here, on HN). And of course we should not forget that the
first "artificial neuron", described by Pitts and McCulloch in 1938 (long
before everything else of the sort) was a propositional logic circuit, because
at the time the models of human cognition were based on the propositional
calculus. The problem with McCarthy's programme, of logic-based AI, is that logic is full
of incompleteness and NP-hardness results, and the more expressive power you
demand from a logic language, the more of those endless pits of undecidability
and despair you fall down. So work in the field advanced veerrryyy slooowwllyyy
and of course much of it was the usual kind of incremental silly-walk stuff I
point out in the comment above. To make matters worse, while significant
academic results drip-dripped slowly and real-world applications were few and
far between, you had prominent researchers overpromising and launching
themselves into wild flights of fancy with abandon based on very early actual
results (certainly not McCarthy! and I don't want to point fingers but cough
Marvin Minsky cough). Then this wretched dog by the name of Sir James Lighthill :spits: was
commissioned by the British Science Research Council, the holders of the Spigot
of the Tap of Funding, to write a report on the progress of AI reserach and the
report was full of misunderstandings and misrepresentations and the Spigot was
turned off and logic-based AI research died. Not just logic-based AI-
Lighthill's :spits: report is the reason the UK doesn't have a robotics sector
to speak of today. Then, while all this was happening in the US and Europe, the
Japanese caught the bug of logic-based AI and they decided to spend a bunch of
money to corner the market for computers like they had with electrical devices
and automobiles, and they instituted something called the Fifth Generation
Computer project (special-purpose computer architectures to run logic
programming languages). That flopped and it took with it one of the few
branches of classical AI that had actually delivered, automated theorem proving. The first link I posed in the comment above is to a televised debate between
Lighthill on the one side and on the other side John McCarthy, Donald Michie
(dean of AI in the UK) and er, some other guy from cognitive science in the US,
I always forget his name and I'm probably doing him a disservice. You may want
to watch that if you are curious about what happened. Pencil pushers without an
inkling of understanding killed logic-based AI research is what happened. That
was a bit like the comet that killed the dinosaurs and gave the mammals a
chance. Meaning those adjacent to AI research directions, like probabilistic
reasoning, connectionism and pattern recognition found an opening and they took
their chance and dominated research since then. I am well aware of the
connotations of my own metaphor. What can I say? Dinosaurs are cool. Ask any
five-year old to explain why. |
Can a sort of vaguely type theory based - and I mean like in the sense of programming be used to reason about law and the like?
Like suppose some article says a man should pay 20% income tax but it says in some other act of some other law that a man shall pay 30% income tax. Like obviously I'm just giving an example but I mean like long cryptic legalese busting. Can we detect contradictions or show that the law or agreement esp like say something like TPP or whatever is inconsistent, by defining types and transactions?
I'm sorry I couldn't word it better. But I hope you get a gist of what I'm saying.