Florian Rabe
------------

As to TPTP HOL:

1. A very simple context-free grammar should be used to give the structure 
of terms. This will be similar to Chris et al.'s original grammar and permit 
lots of nonsense.

2. A precise specification of valid formulas should be given in Twelf (or 
a simi lar tool). This will be similar to the signature I have attached
See below for the attachment.

3. Import and export filters for Twelf are easy to write.

4. Then, TPTP problems can be given in the simple TPTP syntax and imported 
into Twelf for type-checking. Once type-checked, the simple grammar can be 
used to parse the TPTP problems.

Attachment
----------
%% type to hold HOL types
T : type.
%% base types
i : T.
o : T.

%% HOL arrow
> : T -> T -> T.
%% one LF type for every HOL type
U : T -> type.
%% HOL lambda
^ : (U A -> U B) -> U (A > B).
%% HOL application
@ : U (A > B) -> U A -> U B.

%% simple constants
true : U o.
false : U o.
~ : U o -> U o.
binary ops : U o -> U o -> U o.

%% equality (with implicit argument A: T)
equal : U A -> U A -> U o.
%% equality of types
equalT : T -> T -> U o.

%% quantifiers (with implicit argument A: T)
fa : (U A -> U o) -> U o.
ex : (U A -> U o) -> U o.
%% quantification over types
faT : (T -> U o) -> U o.
exT : (T -> U o) -> U o.

%% description and choice; here the semantics is not clear, treatment of empty set?
desc : (U A -> U o) -> U A.                             %% assign with every set an element
choi : ((U A -> U o) -> U o) -> (U A -> U o).           %% assign every set of sets, a set of witnesses

%% one proof type per proposition
theorem : U o -> type.
%% if a prover wants to return a proof object, it must supply a signature that extends the above signature with proof rules

%% example definition, union of two sets (square brackets are the LF lambda)
union = [X:U A -> U o] [Y:U A -> U o] [a: A] X a or Y a.

%% example theorem, commutativity of and
comm_and : theorem ( fa [x:U o] fa [y:U o] ( (x and y) equal (y and x) ) ).