I am mainly interested in understanding various forms of reasoning at a cognitive level. Questions I am interested in are:
Furthermore I have interests in partiality and paradoxes, philosophical issues, and economics.
Some project ideas are listed below.
2. From Planning to Automated Programming
3. Solving the Mutilated Checkerboard Problem
4. A Model Generator for First-Order Logic
5. Modelling Fallacies of Human Reasoning
Knowledge required: knowledge in AI and logic are useful
Brief Description: One of the reasons for the efficiency of automated theorem systems is the
usage of good heuristics. There are different semantic heuristics such as
set of support which make use of additional knowledge about the problem at
hand. For instance, the set of support heuristic assumes that a set of axioms
is consistent. There are also heuristics used which
work well in general without making any additional assumptions. A
heuristic which seems to be generally useful is to `keep things simple'
such as prefer short clause sets over long ones.
Study for simple propositional logic systematically the benefit of
different heuristics by considering the class of all possible problems
rather than testing the heuristics on a sample set.
Languages and/or other Software: CommonLisp would be particularly well-suited
Literature: Manfred Kerber: Heuristics for Resolution in
Propositional Logic, forthcoming.
Knowledge required: Knowledge in AI
Brief Description: Planning has been studied in AI since the
1970's. There are also approaches to extend it to automated program
construction. The idea is to use planning techniques and to generate
a program which satisfies a Hoare triple {A}P{B}. The idea in this
project would be to use planning techniques and generate simple
programs which satisfy the specification. Unlike other approaches the
program has to be guaranteed to do what it is supposed to do.)
Languages and/or other Software: e.g., Lisp, Prolog, ...
Knowledge required: knowledge in logic required
Brief Description: John McCarthy gave in 1964 a challenge problem to
automated reasoning systems, the so-called mutilated checkerboard
problem. This problem exemplifies that a good representation is
essential for solving a problem (this is true not only for reasoning
systems but for any system involving search). In this project students
should study the formal relationship between different representations
of the same problem in order to study the question what the "best"
possible representation to a problem may be. To this end the problems
must be formally represented and proved.
Languages and/or other Software: Any
Literature: Manfred Kerber and Martin Pollet.
A tough nut for mathematical knowledge management.
In Michael Kohlhase, editor, Mathematical Knowledge Management
-- 4th International Conference, MKM 2005, pages 81-95, Bremen, Germany,
2006. Springer, LNAI 3863.
Knowledge required: knowledge in logic required
Brief Description: Roughly speaking a model generator is a system that tries to generate
a finite model for a given set of first-order formulae. This is
essentially done by systematically searching in the space of possible
models, given by universes and interpretations. At first the system
tries whether there is a one-element universe, if not whether there is
a two-element one and so on. In order to be efficient in a huge search
space, choices have to be made in an intelligent way in order to
recognise dead ends as early as possible. Furthermore possibly
existing symmetries should be considered in order to minimise the
search effort. In this project a model generator is to be designed and
implemented.
An interesting idea is to use an efficient propositional logic
satisfiability checker like zChaff and if possible to generate a
first-order model from the propositional logic.
Languages and/or other Software: Any
Literature: John Slaney.
FINDER: Finite domain enumerator-system description.
In Alan Bundy, ed., Proc. of the 12th CADE, Nancy 1994,
p. 798-801. Springer Verlag.
zChaff: http://www.princeton.edu/~chaff/zchaff.html
Knowledge required: in particular AI
Brief Description: The development of classical logic was at least partially motivated by
the attempt to model aspects of human reasoning. However, classical
logic is not adequate to model human deduction (and is surely even
less appropriate for modelling other reasoning modes). One of the
problems is that in classical logic quite common and generally
accepted schemata of reasoning like modus ponens (from "A" and
"A implies B" it is possible to conclude "B") are
equivalent to less familiar one (like from "not B" and
"A implies B" it is possible to conclude "not
A"). However, applying the latter one causes much more
problems to human beings and an argument built up on the second form
is much likely to be faulty than one built up on modus ponens.
Such effects have been studied in detail by Braine et al. [Braine78], [Braine,Reiser,Rumain84] and Johnson-Laird, Byrne [Johnson-Laird,Byrne91].
In the proposed project the most recent literature has to be found and
studied, then it is aimed to develop from the cognitive model of the
reasoning process found there a prototype that can reproduce some of
the phenomena. In particular it would be interesting to investigate
the increase of error frequency of human deduction under time
pressure.
Languages and/or other Software: CommonLisp, Pop11, or Prolog are particular well-suited
Literature: [Braine78]
Martin D.S. Braine.
On the relation between the natural logic of reasoning and standard logic.
Psychological Review, 85(1):1-21, 1978.
[Braine,Reiser,Rumain84]
Martin D.S. Braine, B.J. Reiser, and B. Rumain.
Some empirical justification for a theory of natural propositional logic.
Psychological Learning Motivation,
18(1):313-371, 1984.
[Johnson-Laird,Byrne 91] Philip Nicholas
Johnson-Laird and Ruth M.J. Byrne.
Deduction. Lawrence Erlbaum Associates Ltd., Hove, UK, 1991.
