argumentation corpus

[gusl]

I've designed an XML format for the formalization of arguments. It's still very rough.

taken from Reproductive Sex as Reckless Endangerment:


< premise> Two actions in the same situation are morally equivalent if they have the same predictable effect.
< formalization>< gustavo>
forall A1, A2 : action (PE(A1)=PE(A2) -> ME(A1,A2))
< /gustavo>< /formalization>
< /premise>
< premise>Creating a being that you know will die at a particular time has the same predictable effect as creating a being and then killing it at that time.< /premise>
< formalization>< gustavo>
PE(act1) = PE(act2)
< /gustavo>< /formalization>
< conclusion> To create a being that you know will die at a particular time is morally equivalent to creating such a being and then killing it at that time.< /conclusion>
< formalization>< gustavo>ME(act1,act2)
< /gustavo>< /formalization>
< inference-type-annotation>
< gustavo>UIMP< /gustavo>
< /inference-type-annotation>

< ontology>

< predicate>
< symbol>ME< /symbol>
< arity>2< /arity>
< input-types>action,action< /input-types>
< string>"$1 is morally equivalent to $2"< /string>
< /predicate>

< function>
< symbol>PE< /symbol>
< arity>1< /arity>
< type>action->predictable_effect< /type>
< string>"predictable effect of $1"< /string>
< /predicate>

< atom>
< symbol>act1< /symbol>
< type>action< /type>
< string>To create a being that you know will die at a particular time< /string>
< /atom>

< atom>
< symbol>act2< /symbol>
< type>action< /type>
< string>To create such (anaphor) a being and and kill it at that (anaphor) time< /string>
< /atom>

< /ontology>





It is an open question what set of inference tags will work best.

At first, I thought FOL rules would be enough (MP, MT, UI, etc). But even something as simple as the "Socrates is mortal" argument sits a bit awkward in that scheme: while it feels like one step to us, in FOL it's 2.

There are so many syllogistic forms, etc., which we take for granted. Sure, they could be formalized in FOL, but that's not very natural. In the case of "Socrates is mortal", the syllogism corresponds to a U.I. followed by an M.P.: but that's not how people think! The form of the syllogism precedes its formalization, so that is the right level of chunking.

The good news is that intro logic books provide tons of examples, and could serve as an initial corpus.

Comments

[fancybred.livejournal.com]

There's been a lot of recent work on "focusing" proofs, which addresses the problem of finding the right level of chunking. You might be interested in the paper "Human-readable, machine-verifiable proofs for teaching constructive logic" by Abel, Chang, and Pfenning.

[gustavolacerda.livejournal.com]

IIRC, in Coq, you can do intros. . It is an interesting idea, that ordinary human reasoning uses this tactic!