Appendix B: KE Text Syntax

{ke-file}         ::= ""

                   | {full-expression}

                   | {full-expression} {ke-file}

{full-expression} ::= {expression} "."

{expression}      ::= {directive}

                   | {predicate-assertion}



{directive} ::= {assert-mode-directive}

     | {constant-directive}

             | {in-mt-directive}

             | {default-mt-directive}

             | {assertion-direction-directive}

             | {assertion-truth-directive}

     | {include-ke-file-directive}

             | {kill-directive}

             | {rename-directive}

             | {formula-directive}



{assert-mode-directive} ::= {enter-directive} | {delete-directive}

{enter-directive} ::= {enter-keyword}

{enter-keyword} ::= "enter"



{delete-directive} ::= {delete-keyword}

{delete-keyword} ::= "delete"



{in-mt-directive} ::= {in-mt-keyword} ":" {microtheory}

{in-mt-keyword} ::= "in mt"

{microtheory} ::= a string representing an instance of #$Microtheory



{default-mt-directive} ::= {default-mt-keyword} ":" {microtheory}

{default-mt-keyword} ::= "default mt"

{microtheory} ::= a string representing an instance of #$Microtheory



{assertion-direction-directive} ::= {assertion-direction-keyword} ":"

                                   {assertion-direction-indicator}

{assertion-direction-keyword} ::= "d" | "al" | "access level" | "direction"

{assertion-direction-indicator} ::= ":" {assertion-direction-indicator-keyword}

                                 | {assertion-direction-indicator-keyword}

{assertion-direction-indicator-keyword} ::= "0" | "forward"

                                         | "4" | "backward"

                                         | "code" | "unknown"



{assertion-truth-directive} ::= {assertion-truth-keyword} ":"

                               {assertion-truth-indicator}

{assertion-truth-keyword} ::= "truth value" | "tv"

{assertion-truth-indicator} ::= ":" {assertion-truth-indicator-keyword}

                             | {assertion-truth-indicator-keyword}

{assertion-truth-indicator-keyword} ::= ":default" | ":monotonic" | ":unknown"



{constant-directive} ::= {constant-keyword} ":" {constant-name}

{constant-keyword} ::= "constant" | "unit"

{constant-name} ::= a string representing the name of the constant



{kill-directive} ::= {kill-keyword} ":" {existing-constant}

{kill-keyword} ::= "kill"

{existing-constant} ::= a string representing an existing constant



{rename-directive} ::= {rename-keyword} ":" {existing-constant}

                                           {new-constant-name-string}

{rename-keyword} ::= "rename"

{existing-constant} ::= a string representing an existing constant

{new-constant-name-string} ::= a quoted string of the new constant name



{include-ke-file-directive} ::= {include-ke-file-keyword} ":" {filepath}

{include-ke-file-keyword} ::= "include"

{filepath} ::= path to the file



{formula-directive} ::= {formula-keyword} ":" {formula}

{formula-keyword} ::= "f" | "el" | "formula"

{formula} ::= a CycL formula



{predicate-assertion} ::= {pred-assertion-arity-2}

                       | {pred-assertion-arity-3}

                       | {pred-assertion-arity-4}

                       | {pred-assertion-arity-5}

{pred-assertion-arity-2} ::= {binary-pred} ":" {atoms}

{atoms} ::= {atom} | {atom} {atoms}

{atom} ::= fort | string | number | ?TODO?

{pred-assertion-arity-3} ::= {ternary-pred} ":" {atom-pairs}

{atom-pairs} ::= {atom-pair} | {atom-pair} {atom-pairs}

{atom-pair} ::= "(" {atom} {atom} ")"

{pred-assertion-arity-4} ::= {quaternary-pred} ":" {atom-triplets}

{atom-triplets} ::= {atom-triplet} | {atom-triplet} {atom-triplets}

{atom-triplet} ::= "(" {atom} {atom} {atom} ")"

{pred-assertion-arity-5} ::= {quintary-pred} ":" {atom-quartets}

{atom-quartets} ::= {atom-quartet} | {atom-quartet} {atom-quartets}

{atom-quartet} ::= "(" {atom} {atom} {atom} {atom} ")"