Tau Control Panel
- 1 Show the input frame for argument and theorem proof input
- 2 Reset the control panel display
- 3 Enter the name of a KB to create
- 4 Select so other users and other sessions can access the newly created KB
- 5 Select the formula display or input syntax
Proof Input
- 1 Enter formulas to prove
- 2 Begin the proof
- 3 Select KB from which to draw premises for argument proof; NONE proves theorems
- 4 Select the formula input syntax
- 5 Generate a detailed proof trace
- 6 Interpret propositional constants as zero-argument predicate applications
KB Content Input
- 1 Enter formulas to record
- 2 Record the formulas
- 3 Select KB in which to record formulas
- 4 Select the formula input syntax
- 5 Echo the KB contents after new formulas are added
- 6 Interpret propositional constants as zero-argument predicate applications
Tau Formula Syntaxes
KIF (Prefix)
The standard KIF 3 syntax has a Lisp-like S-Expression syntax.
Grammar
(forall ?VAR Formula)
- Universally quantified Formula
(forall (?VAR1 ?VAR2 ...) Formula)
- Universally quantified Formula binding multiple variables
(exists ?VAR Formula)
- Existentially quantified Formula
(exists (?VAR1 ?VAR2 ...) Formula)
- Existentially quantified Formula binding multiple variables
(=> AntecedentFormula ConsequentFormula)
- Material implication between Antecedent and Consequent
(<= ConsequentFormula AntecedentFormula)
- Material implication between Antecedent and Consequent (reversed order)
(<=> Formula Formula)
- Logical equivalence of Formulas
(and Formula*)
- Conjunction of Formulas--multiary
(or Formula*)
- Disjunction of Formulas--multiary
(not Formula)
- Negation of Formula--unary
(Predicate Term*)
- Application of predicate to argument Terms
(= Term Term)
- Equation of Terms
(/= Term Term)
- Disequation of Terms
(Function Term*)
- Application of Function to argument Terms
; Single-line comment
- All characters beginning with a semicolon to the end of line on which it appears are ignored
#| Multi-line comment |#
- All characters from the pair of characters "#|" to the first following occurrence "|#" are ignored.
Multi-line comments do not nest.
Examples
(=> (human ?H) (mortal ?H))
(forall (?X ?Y ?Z)
(=>
(and (= ?X ?Y) (not (= ?Y ?Z)))
(not (= ?X ?Z))))
Tau (Infix)
Grammar
forall ?VAR Formula
- Universally quantified Formula
forall (?VAR [, ?VAR]*) Formula
- Universally quantified Formula binding multiple variables
exists ?VAR Formula
- Existentially quantified Formula
exists (?VAR [, ?VAR]*) Formula
- Existentially quantified Formula binding multiple variables
~Formula
- Negation of Formulas
Formula & Formula
- Conjunction of Formulas
Formula | Formula
- Disjunction of Formulas
AntecedentFormula => ConsequentFormula
- Material implication between Antecedent and Consequent
ConsequentFormula <= AntecedentFormula
- Material implication between Antecedent and Consequent (reversed order)
Formula <=> Formula
- Logical equivalence of Formulas
Formula <~> Formula
- Logical opposition of Formulas (exclusive OR)
Predicate(Term [, Term]*)
- Application of predicate to argument Terms
Term = Term
- Equation of Terms
Term /= Term
- Disequation of Terms
(Formula)
- Parentheses can be used to override operator precedences
Function(Term [, Term]*)
- Application of Function to argument Terms
Formula; Formula; ...
- Multiple formulas are separated by semicolons
// Single-line comment
- All characters beginning with two adjacent slashes to the end of line on which they appear are ignored
/* Multi-line comment */
- All characters from the pair of characters "/*" to the first following occurrence "*/" are ignored.
Multi-line comments do not nest.
Infix Operator Precedences
- lowest precedence / loosest binding
1R: forall1R: exists1R: =>2R: <=3L: <=>3L: <~>4M: |5M: &6: ~7: (Formula)- highest precedence / tightest binding
1-7: Distinct precedence levels
R: Right associative
L: Left associative
M: Multi-ary: Adjacent uses create single generalized (multi-ary) conjunction or disjuntion
Examples
human(?H) => mortal(?H);
forall (?X, ?Y, ?Z)
?X = ?Y & ?Y /= ?Z => ?X /= ?Z