Deimos: Syntax

This document describes the syntax accepted by this implementation of Defeasible Logic.

Whitespace and Comments

Before or after any token can be any amount of whitespace. Comments are treated as whitespace.

	comment1
		::= "%" {anything-not-"\n"} ("\n" | end-of-file)

	comment2
		::= "/*" comment2'
	comment2'
		::=   "*/"
                    | any-character comment2'

Identifiers

 	name1
		::= lower-case-letter {letter | digit | "_"}

	name2
		::= upper-case-letter {letter | digit | "_"}

Literals

	constant
		::=   name1

        variable
		::=   name2

        argument
		::=   constant
                    | variable

        argList
		::= "(" argument {"," argument} ")" 

        literal
		::= ["~"] name1 [argList]

	prolog_literal
		::=  ["neg"] name1 [argList]

Rules

	antecedent
		::= | "{" "}"
		    | "{" literal {"," literal} "}"
		    | literal {"," literal}
	            | nothing

	rule
		::= antecedent ("->" | "=>" | "~>") literal

	prolog_antecedent
		::=   "true"
		    | prolog_literal {"," prolog_literal}

	prolog_rule
		::= prolog_literal (":-" | ":=" | ":^") prolog_antecedent
 

Labels and Priorities

	label
		::= name2
		
	priority
		::= label ">" label

Theories

	fact
		::= prolog_literal | literal

	rule'
		::= prologRule | rule

	labeled_rule
		::= [label ":"] rule'

	prolog_superiority
		::= "sup" "(" "("  rule' ")" "," "(" rule' ")" ")"
   
	statement
		::=   prolog_superiority
		    | labeled_rule
                    | priority
		    | fact

	theory
		::= {statement "."}

Here are some example Defeasible theories that can be parsed:

% preferred (Deimos) syntax

      emu.
      emu => heavy.
      emu -> bird.
R1:   bird => flies.
R2:   heavy ~> ~flies.
      R2 > R1.

 

%  d-Drolog syntax

emu.
bird :- emu.
heavy := emu.
flies := bird.
neg flies :^ heavy.
sup((neg flies :^ heavy), (flies := bird)).

 

% mixing both

      emu.
      heavy := emu.
      bird :- emu.
R1:   flies := bird.
R2:   neg flies :^ heavy.
      R2 > R1.

Tagged Literals

A query to this system is a tagged literal; a literal to be proved, tagged by the level of proof required. At present the literal must be grounded, that is contain no variables.

	proof_symbol
		::= "D" | "d" | "da" | "S" | "dt"

	tagged_literal
		::= ("+" | "-") proof_symbol literal