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, Argumentative, Athena, bCisive, Carneades, Collam, and Rationale.  Web applications include Argumentum, bCisive Online, Cohere, Debategraph, truthmapping.com, Compendium, Argunet, MIT’s Deliberatorium, debatewise.com 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 Deduction, the 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.