The Logical Parts

Any non-predefined signature symbol used in a problem has to be defined in a the declaration part. Then the logical part may provide a formulation of the problem by formulae as well as by some clause normal forms. In addition, proofs for the conjecture stated by the formulae (clauses) may be contained.

logical_part	::=	{symbol_list}
		{declaration_list}
		{formula_list}$^\ast$
		{clause_list}$^\ast$
		{proof_list}$^\ast$

As mentioned before, non-predefined signature symbols have to be declared in advance. Since the current scope of the syntax mainly covers first-order logic, we are concerned with function and predicate symbols and non-standard operators and quantifiers. The usual first-order operators and quantifiers are predefined. In addition, there is a unique symbol for equality, see below.

symbol_list	::=	list_of_symbols.
		{functions[fun_sym | (fun_sym,arity)
		{, fun_sym | (fun_sym,arity)}$^\ast$].}
		{predicates[pred_sym | (pred_sym,arity)
		{, pred_sym | (pred_sym,arity)}$^\ast$].}
		{sorts[sort_sym {,sort_sym}$^\ast$].}
		{operators[ op_sym | (op_sym,arity)
		{, op_sym | (op_sym,arity)}$^\ast$].}
		{quantifiers[quant_sym | (quant_sym,arity)
		{, quant_sym | (quant_sym,arity)}$^\ast$].}
		end_of_list.

All declared symbols have to be different from each other and from all terminal and predefined symbols.

We support a rich sort language that may be introduced by a declaration part. We do not allow free variables in term declarations, but polymorphic sorts.

declaration_list	::=	list_of_declarations.
		{declaration}$^\ast$
		end_of_list.
declaration	::=	subsort_decl | term_decl | pred_decl | gen_decl
gen_decl	::=	sort sort_sym {freely} generated by func_list.
func_list	::=	[ fun_sym {,fun_sym}$^\ast$]
subsort_decl	::=	subsort(sort_sym,sort_sym).
term_decl	::=	forall(term_list,term). | term.
pred_decl	::=	predicate(pred_sym{,sort_sym}+).
sort_sym	::=	identifier
pred_sym	::=	identifier
fun_sym	::=	identifier

Concerning the term declarations, we assume that all terms in term_list are variables or expressions of the form sort_sym(variable).

Now there are two types of formulae: Axiom formulae and conjecture formulae. If the status of the problem (see below) states ``unsatisfiable'' it refers to the clause normal form resulting from the conjunction of all axiom formulae and the negation of the conjunction of all conjecture formulae. Of course, ``satisfiable'' means that the overall formula has a model.

formula_list	::=	list_of_formulae(origin_type).
		{formula({term}{,label}).}$^\ast$
		end_of_list.
origin_type	::=	axioms | conjectures
label	::=	identifier

We assume that all formulae are closed, so we do not allow free variables inside a formula expression.

Quantifiers always have two arguments: A term list and the subformulae. The term list is assumed to be a variable list (or a list of variables annotated with a sort) for the usual first-order quantifiers, however, one could easily imagine non-classical quantifiers, where ``quantification'' over real terms makes sense.

term	::=	quant_sym(term_list,term) | symbol | symbol(term{,term}$^\ast$)
term_list	::=	[term{,term}$^\ast$]
quant_sym	::=	forall | exists | identifier
symbol	::=	equal | true | false | or | and | not | implies | implied | equiv | identifier

We support disjunctive normal form as well as clause normal form. Even clauses have to be written as their corresponding formulae, in particular all variables have to be bound by the leading quantifier. Our experience with problems stated by a set of clauses shows that this helps to detect flaws, e.g., if accidentally it was forgotten to declare some constant that would then be considered as a variable. Since free variables are not allowed, this case is detected in our syntax.

clause_list	::=	list_of_clauses(origin_type,clause_type).
		{clause({cnf_clause | dnf_clause}{,label}).}$^\ast$
		end_of_list.
clause_type	::=	cnf | dnf
cnf_clause	::=	forall(term_list,cnf_clause_body) | cnf_clause_body
dnf_clause	::=	exists(term_list,dnf_clause_body) | dnf_clause_body
cnf_clause_body	::=	or(term{,term}$^\ast$)
dnf_clause_body	::=	and(term{,term}$^\ast$)

In case of cnf_clause_body and dnf_clause_body we assume all subterms generated for term to be literals.

The alphabet allowed to compose identifiers is restricted to letters, digits and the underscore symbol.

identifier	::=	{letter | digit | special_symbol}+
letter	::=	a -z | A -Z
arity	::=	-1 | number
number	::=	{digit}+
digit	::=	0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
special_symbol	::=	_