Argumentation Systems

This Monday on the train I saw a colleague of mine, Gustaaf Haan, who, as I found out, has a degree in Argumentation Theory and gives lessons to lawyers. Since then I've been trying to sell him some of my reductionistic ideas, such as:

* we can in principle formalize all forms of argument: Leibniz's Calculemus
* most disagreements are irrational, you can't agree to disagree, etc.


I imagine that this area of "Argumentation Systems" encompasses widely different projects, from "using XML to parse the logical structure of an argument in a text; or for annotating responses and criticisms" to "game-theoretical semantics's of argumentation logics".


Some relevant links:

On argumentation games:
Johan van Benthem - Argument and Procedure (an interesting project would be interrogation strategies to catch a liar, by making it computationally hard for him to improvise a consistent story) and Johan van Benthem - What Logic Games are Trying to Tell us
Wikipedia - Logic & Games in general

IT solutions to Rhetoric :-) (i.e. systems to help resolve arguments more objectively):
Gordon, Karacapilidis - The Zeno Argumentation Framework

Gerard Vreeswijk - Abstract Argumentation Systems
this one has "defeasible proofs"

I also remember reading something by John McCarthy along these lines.


I'll see if I can do my Dialogue Systems project on argumentation systems. These ideas are close and dear to me.

Two nice, contentful academic personal websites

Alessio Guglielmi

...
My second research objective is to come up with useful, interesting notions of identity of proofs. It is embarrassing for proof theory that the natural question of `when are two proofs to be considered identical?´ lacks good answers.* (This question is tightly connected to the equally non-well-understood problem of deciding when two algorithms are the same.) One reason for our embarrassment is that the notion of normalisation available, viz. cut elimination, is inadequate to decide the question; I believe that the problem is that this is the only (reasonable) normalisation notion available in the sequent calculus and natural deduction. Thanks to its finer granularity, the calculus of structures offers several natural new notions of normalisation, this way improving our ability to study new concepts of identity.
...

Finally someone addresses my question about proof uniqueness! Google wasn't helping me at all, so I had to find it by accident.



Dan Sperber researches language, cognition, culture and evolution

computability, model-checking, and human reasoning

Halpern, Vardi - Model Checking vs Theorem-Proving: A Manifesto suggests model-checking as a cheaper alternative, since theorem-proving is NP-complete. This seems to me to be more like how humans reason, precisely for the same reason (unlike some people, I believe our brains are classical computers).

Towards a `Model Computation Manifesto'

Computability Logic

education

R.M. Sperandeo-Mineo - LEARNING PHYSICS VIA MODEL CONSTRUCTION


from the QED Manifesto

The development of mathematical ability is notoriously dependent upon
`doing' rather than upon `being told' or `remembering'. The QED system
will provide, via such techniques as interactive proof checking
algorithms and an endless variety of mathematical results at all
levels, an opportunity for the one-on-one presenting, checking, and
debugging of mathematical technique, which it is so expensive to
provide by the method of one trained mathematician in dialogue with
one student. QED can provide an engaging and non-threatening framework
for the carrying out of proofs by students, in the same spirit as a
long-standing program of Suppes at Stanford for example[link mine]. Students will
be able to get a deeper understanding of mathematics by seeing better
the role that lemmas play in proofs and by seeing which kinds of
manipulations are valid in which kinds of structures. Today few
students get a grasp of mathematics at a detailed level, but via
experimentation with a computerized laboratory, that number will
increase. In fact, students can be used (eagerly, we think) to
contribute to the development of the body of definitions and proved
theorems in QED.

Intelligence as Abstraction

mathemajician reminded me (i.e. I reminded myself by reading him) to write up my notes about intelligence, since he is trying to write a philosophical paper on intelligence at the moment.

Don't pay attention to the circularity: it's a necessary part of the philosophical process.

intelligence: the ability to create and use abstraction.
abstraction: a central feature of intelligence, whose purpose is to economize computational resources by reusing similar structures.
redundancy: randomness deficiency. Redundancy is the property of, for example, structures with similar parts. Data without redundancy is simply random noise. Redundancy is a prerequisite for meaningfulness: without redundancy, language would be unlearnable. Nature herself is highly redundant: if it weren't, science wouldn't work. See: Information Theory, Kolmogorov Complexity, Learning as Compression.

Hardcoding is the lack of abstraction. It is more efficient for specialized behavior. So it's a trade-off. However, abstraction, being a conscious process, allows a greater degree of control and flexibility; not to mention the freedom to use one's intelligence & knowledge on novel applications. Abstraction allows true "creativity".


SOME DOMAINS:

behavior type--> domain	intelligent	unintelligent
language is known to be an area in which our processing (including some "reasoning") is largely automatic and unconscious.	Abstract thought away from language. Try to generate utterance from the abstract thought.	Think in their mother tongue. Translate word by word. Sometimes even translate things like: "het weer" => "the again".
music	Solfège: map songs to sequence of abstract notes relative to the key. Once a song has been learned, a solfeger can play it in any key and on any instrument. Solfege taps into the efficient language-processing module by encoding notes as syllables (we can process language representations), which may aid not only memorization, but also improvisation and composition (after enough solfeging in a musical idiom, the musician learns a language of syllable patterns, which he can use to create novel phrases and decode them back into music).	map: songs -> sequence of finger positions
science and mathematics	* meta-science * applying proof theory to analysis (see Kohlenbach). * A good design of Mathematical Concepts may reduce cognitive burden (i.e. economize computational resources)
programming	meta-programming, modular design of code AND data, intelligent design patterns, high-level languages: code is close to specifications	hardcoding, low-level languages

intelligence (refined definition): the ability to represent abstract structures on their own. This is extremely difficult in some cases, if only because of the computational load. But abstract imagination seems inherently difficult: how can one imagine a structure which is inherently abstract? How can one picture a tree which could have either 3 or 4 branches, no more, no less? This can perhaps be done by imagining a flickering picture.

reflection and self-improvement

humans seem to be happy as long as they are learning optimally. If challenges are too hard or too easy, they will get bored.

Manfred Kerber -Mathematical Reasoning: Machines vs Humans

Manfred Kerber -Mathematical Reasoning: Machines vs Humans