Argumentation and Mathematics

With regard to argumentation, some representation formats include the Argument Interchange Format (AIF), Argument Markup Language (AML), Legal Knowledge Interchange Format (LKIF) and the Proof Markup Language (PML).

Argument mapping and visualization software include Araucaria, ArgumentativeAthenabCisiveCarneades, Collam, and Rationale.  Web applications include ArgumentumbCisive Online, Cohere, Debategraph,, Compendium, Argunet, MIT’s and CoPe_it.

Additionally, many computational mathematics software include their own proof formats such as HOL, Mizar, PVS, Coq, Otter/Ivy, Isabelle/Isar, Alfa/Agda, ACL2, PhoX, IMPS, Metamath, Theorema, Lego, Nuprl, Ωmega, B method, and Minlog.

At the 23rd International Conference on Automated Deductionthe first workshop on proof exchange for theorem proving (PxTP) occurred with goals that included facilitating the exchange of knowledge, such as machine-checkable proofs, between automated reasoning systems. Furthermore, the workshop indicated that “emerging work from several groups proposes standard meta-languages or parametrized formats to achieve flexibility while retaining a universal proof language.”  Proof formats, meta-languages and logical frameworks for proofs were discussed.

Interestingly, argumentation formats can include mathematical proofs in their expressiveness.  Knowledge representation formats can be devised capable of simultaneously representing conversational, mathematical, scientific, legal and political forms of argumentation and debate.


One thought on “Argumentation and Mathematics

  1. Pingback: Argumentation and Science | Phoster Development Blog

Leave a Reply

Please log in using one of these methods to post your comment: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s