Phobos: Syntax

This document describes the syntax accepted by this implementation of Plausible 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]

Formulas

   formula
      ::=   formula "->" consequent
          | consequent

   consequent 
      ::=   consequent "|" disjunct
          | disjunct

   disjunct 
      ::=   disjunct "&" conjunct
          | conjunct

   conjunct 
      ::=   literal
          | "(" formula ")"
          | "~" conjunct
          | "/\" formulaSet  
          | "\/" formulaSet

   formulaSet 
      ::=   "{" "}"
          | "{" formula {"," formula} "}"

Rules

   rule
      ::= strictRule | plausibleRule | defeater

   strictRule 
      ::= antecedent "->" formula

   plausibleRule 
      ::= antecedent "=>" formula

   defeater 
      ::= antecedent "-\" formula

   antecedent 
      ::=   formulaSet
          | consequent

Descriptions

Descriptions are stored in text files with names that end in ".d".

   description    
      ::= {dStatement "."}
      
   dStatement      
      ::= fact | plausibleRule | defeater

   fact
      ::= formula

Here is an example Plausible description that can be parsed:

% Siberian huskies and other mutts (uses variables!)

m(r).                        % Rover is a mutt.
sh(n).                       % Nanook is a Siberian husky.
    
m(X) -> d(X).             % Mutts are dogs. 
sh(X) -> d(X).            % Siberian huskies are dogs.

d(X) => b(X).             % Dogs usually bark.
sh(X) => ~b(X).           % Siberian huskies usually do not bark.

sh(X) => h(X).            % Siberian huskies are usually huge.
m(X) => ~h(X).            % Mutts are not usually huge.
{d(Y), b(Y)} => f(X, Y).  % Most things fear barking dogs.
{d(Y), h(Y)} => f(X, Y).  % Most things fear huge dogs.
{h(X), d(X)} => ~f(X, Y). % Huge dogs don't usually fear anything.

Theories

Theories should be automatically generated from descriptions. The user only needs to add priorities.

Theories are stored in text files with names that end in ".t".

A Theory statement usually ends in ".", but some (for research hacking purposes) need to bypass the usual consistency checks. These end with a "!".

   theory
      ::= {statement "." | statement "!"}
   
   statement 
      ::=   rule 
          | label ":" rule
          | priority

   priority 
      ::= label ">" label

   label
      ::= name2

Here is an example Plausible theory that can be parsed:

% Siberian huskies and other mutts (uses variables!)

R1:  {} -> m(r).               % Rover is a mutt.
R2:  {} -> sh(n).              % Nanook is a Siberian husky.
     
R3:  {m(X)} -> d(X).           % Mutts are dogs. 
R4:  {sh(X)} -> d(X).          % Siberian huskies are dogs.
R5:  {~d(X)} -> ~m(X).         % Anything not a dog is not a mutt.
R6:  {~d(X)} -> ~sh(X).        % Anything not a gog is not a Siberian husky.
R7:  {m(X) | sh(X)} -> d(X).   % If something is a mutt or a Siberian husky, it is a dog.

R8:  {b(Y), d(Y)} => f(X, Y).  % Most things fear barking dogs. 
R9:  {d(X)} => b(X).           % Dogs usually bark.
R10: {d(X), h(X)} => ~f(X, Y). % Huge dogs usually don't fear anything.
R11: {d(Y), h(Y)} => f(X, Y).  % Most things fear huge dogs.
R12: {m(X)} => ~h(X).          % Mutts are usually not huge.
R13: {sh(X)} => h(X).          % Siberian huskies are usually huge.
R14: {sh(X)} => ~b(X).         %  Siberian huskies usually don't bark.
R15: {b(Y) | d(Y), b(Y) | h(Y), d(Y), d(Y) | h(Y)} => f(X, Y).
      % Most things fear something that:
      %    barks or is a dog,
      %    barks or is huge,
      %    is a dog, and
      %    is a dog or is huge

R14 > R9.  % R14 is more specific than R9.
R10 > R8.  % hugeness is more fearsome than loudness.

Tagged Formulas

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

   taggedFormula 
      ::= plusMinus proofSymbol formula
   
   plusMinus 
      ::= "+" | "-"
   
   proofSymbol 
      ::= "d" | "l" | "p" | "s"