InformalArgumentInAgda

Purpose

Discussion 25/3

• Two fronts
  • How to represent arguments
  • Providing shallow scafolding formalization of Contents of arguments (cf. safety case patterns)
• What Agda is good for
  • Parametrization/Abstraction using dependent types
    • Defining primitive predicates
    • Organizing data appearing in arguments e.g. Requirements _for each service_
  • Expectation from industry
    • Guidance on writing down rules
    • Managing the volume of a Case Incl. beauraucratic checking
• Wishes for Agda functionality
  • Allowing reordering of sections in Literate Agda.

Discussion 26/3

• on Representing proofs in GSN
  • M tries to display 1st order logic proof in "D-Case Tool"
• on Need for interpreting formalised object.
• a look at an attempt to construct Robot Arm safty case by a real engineer.
• on Distinguishing making up rules and using rules.

Discussion 29-30/3

• A look at a Accenture requirement-engineering tool with nat. lang. processing.
• Value of trying Nat. Lang. YK: Only a tentative need till engineers learn Formal Language.
  B: Stil helps a lot in readability.

     Some contract have to be written in NL.

• Before natural language tech, Important things are
  • Showing overall structure. Layout (interactive outline-mode)

     Indentation
     Itemization
   (Medicine doc example)
   Goal Structuring Notation 

• How to add the knowledge to lexicons
  e.g. To introducint the word "run", you have to specify - "run" is a 'verb', - it may be used as 'transitive verb',

     - apperaing as in <subj> "run" <obj>, ...
   - it may be used as 'intransitive verb',
     - ...

• Informal text output from formal content is more promissing than the other way round.
• What is wanted may be a simple fill-in form with structure. rather than complicated logical checks.
• The first thing to do is coming up with the structure to be filled-in.
• Do we know any example of such structure? - No.
• The mixfix notation of Agda can already do a lot. NL like expression in Agda should be tried.
• Benefits of using Agda
  • The usual benefits of formalization
    • Beauraucratic checking of details
    • Consistent use of terms, Correct expansion of defined terms, ...
  • Validation of formalization After formalization, we could check whether expected properties are holding or can be proven.
• How to showcase the benefits of Agda
  • Just translate a GSN example in Agda, with just the essentials.
• Trying a deep embedding of basic TT to print out proofs Based on Conor's idea of syntactic terms indexed by their semantic types. Hard to recurse on term structure together with syntactic types

Links

Virginia U Safety Case Repository