McGuinness Oct 17, 2002
4
Issues
nVariable granularity (lcf, pruning, etc)
nDegree of annotation for human readability (human paraphrase in addition to
machine readability)
nAgents should be able to verify proofs
nProofs should be “nestable” and “queryable
and/or reexecutable”
nProof language should be ubiquitous
nProofs should be incremental
nConfidence in proof steps should be
expressible
nDaml-compliant inference engines should respond
to client requests with “reasonable explanation” in the daml language
nIdentifying rules (naming,…)