Safe Haskell	None

Language.Carneades.CarneadesDSL

Synopsis

Documentation

type PropLiteral = (Bool, String)Source

negate :: PropLiteral -> PropLiteral Source

newtype Argument Source

Constructors

Arg ([PropLiteral], [PropLiteral], PropLiteral)

Instances

Eq Argument
Ord Argument
Show Argument

showProp :: PropLiteral -> String Source

type ArgSet = Gr (PropLiteral, [Argument]) ()Source

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:

type Audience = (Assumptions, ArgWeight)Source

type Assumptions = [PropLiteral]Source

type ArgWeight = Argument -> Weight Source

type Weight = Double Source

type PropStandard = PropLiteral -> PSName Source

data PSName Source

Constructors

Scintilla
Preponderance
ClearAndConvincing
BeyondReasonableDoubt
DialecticalValidity

Instances

Eq PSName
Show PSName

type ProofStandard = PropLiteral -> CAES -> Bool Source

newtype ProofStandardNamed Source

Constructors

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

Instances

Eq ProofStandardNamed

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}

applicable :: Argument -> CAES -> Bool Source

acceptable :: PropLiteral -> CAES -> Bool Source

$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:

scintilla :: ProofStandard Source

maxWeightApplicable :: [Argument] -> CAES -> Weight Source

maxWeightPro :: PropLiteral -> CAES -> Weight Source

maxWeightCon :: PropLiteral -> CAES -> Weight Source

preponderance :: ProofStandard Source

clear_and_convincing :: ProofStandard Source

beyond_reasonable_doubt :: ProofStandard Source

dialectical_validity :: ProofStandard Source

psMap :: PSName -> ProofStandard Source

getAllArgs :: ArgSet -> [Argument]Source

getProps :: ArgSet -> [PropLiteral]Source

applicableArgs :: CAES -> [Argument]Source