CarneadesDSL-1.2: An implementation and DSL for the Carneades argumentation model.

Safe HaskellNone

Language.Carneades.CarneadesDSL

Synopsis

Documentation

newtype CAES Source

Constructors

CAES (ArgSet, Audience, PropStandard) 

subset mathcal{L}$ is a propositionally consistent set of literals (i.e., not containing both a literal and its negation) assumed to be acceptable by the audience and emph{weight} is a function mapping arguments to a real-valued weight in the range $[0,1]$. end{definition} This definition is captured by the following Haskell definitions:

newtype ProofStandardNamed Source

Constructors

P (String, PropLiteral -> CAES -> Bool) 

then an argument $a = langle P, E, c rangle$ is emph{applicable} iff begin{itemize} item $p in P$ implies $p$ is an assumption or [,$overline{p}$ is not an assumption and $p$ is acceptable in $C$,] and item $e in E$ implies $e$ is not an assumption and [,$overline{e}$ is an assumption or $e$ is not acceptable in $C$,]. end{itemize} end{definition} begin{definition}[Acceptability of propositions] Given a CAES $C$, a proposition $p$ is emph{acceptable} in $C$ iff $(s ; p ; C)$ is $true$, where $s$ is the proof standard for $p$. end{definition}

Note that these two definitions in general are mutually dependent because acceptability depends on proof standards, and most sensible proof standards depend on the applicability of arguments. This is the reason that Carneades restricts the set of arguments to be acyclic. (Specific proof standards are considered in the next section.) The realisation of applicability and acceptability in Haskell is straightforward: -- begin{code} -- applicable :: Argument -> CAES -> Bool -- applicable (Arg (prems, excns, _)) caes(CAES (_, (assumptions, _), _)) -- = and $ [(p elem assumptions) || (p acceptable caes) | p <- prems ] -- ++ -- [(e elem assumptions) nor (e acceptable caes) | e <- excns ] -- where -- x nor y = not (x || y) -- acceptable :: PropLiteral -> CAES -> Bool -- acceptable c caes(CAES (_, _, standard)) -- = c s caes -- where P (_, s) = standard c -- end{code}

$gamma$; these are assumed to be defined once and globally. This time, we proceed to give the definitions directly in Haskell, as they really only are translitarations of the original definitions.

For a proposition $p$ to satisfy the weakest proof standard, scintilla of evidence, there should be at least one applicable argument pro $p$ in the CAES:

unsafeMatch :: Graph gr => Node -> gr a b -> (Context a b, gr a b)Source