Argumentation Interchange and Representation Formats

Argumentation Community Group,

Existing argumentation and proof representation formats include: Argument Interchange Format (AIF), AIF-RDF, Argument Markup Language (AML), Legal Knowledge Interchange Format (LKIF), Open Mathematical Documents (OMDoc), Proof Markup Language (PML), Thousands of Problems for Theorem Provers (TPTP), and Thousands of Solutions for Theorem Provers (TSTP).

With regard to argumentation, a special topic is the representation of mathematical proofs.  Proof exchange for theorem proving is topical and automated theorem proving technologies include: ACL2, Agda, Automath, Coq, CVC, E, EQP, Gandalf, Isabelle / HOL, IsaPlanner, j'Imp, Jape, KED Theorem Prover, KeY, KeYmeara, LEGO, Leo II, LoTREC, Matita, MetaPRL, Metis, MINLOG, Mizar, NuPRL, Otter, Paradox, PhoX, Prover9 / Mace4, PVS, SAD, Saturate, SNARK, SPASS, Tau, Theorem Checker, Theorem Proving System, Twelf, Typelab, Vampire / Vampyre, Waldmeister, and Yarrow.

Research into argumentation formats and systems can facilitate data motion between automated reasoners, automated theorem provers, computer algebra systems and other advanced software and systems.

With regard to visualizing arguments, argument mapping technologies include: Araucaria, argdf.org, Argumentative, Argunet, Athena, bCisive Online, Carneades, Cohere, Collam, Compendium, CoPe_it, Debategraph, debatewise.com, Deliberatorium, Rationale, truthmapping.com .

We might want to collate a comprehensive list for links on the Community Group's website.  Additionally, such a collated list can convenience comparing and contrasting previous and current approaches as well as discussions about requirements for any new formats or systems.



Kind regards,

Adam