THE INTUITIONISTIC THEOREM PROVER ft (1.23)

The user interface of ft has a Prolog feel to it. All input to ft, from the keyboard or from a file, ends with a period followed by a newline (with optional invisible text in between). Text from the comment character % to the next newline is invisible to ft, as is any text between [ and ]. Comment brackets are nestable. Except for newline after period or as marking the end of a %-comment, whitespace in the input - space, tab, newline - is also invisible to ft and can be inserted wherever you like. A ^C at the end of a string of characters will cause ft to ignore that string when RETURN is pressed. Output is always to stdout. In connection with input from or to files, see echo, read below. ft understands input of three kinds: commands, system variables, formulas. Commands ======== quit End execution. An EOF from stdin is equivalent to quit. set [sysvar value,sysvar value,..] The command set alone gives the current values of the alterable system variables. (To learn the value of a single variable, input the name of that variable.) To change the value of one or several variables, use the syntax exemplified by set ucon 4,allimp 0,timeout 60,echo 1. reset The system variables are reset to their boot values. The main stack, the formula stack, and the save areas are resized to their initial values. read ft attempts to open the indicated file and read input from that file. read can be nested. Input from a file is echoed to the terminal if the system variable echo is true. If echo has value 2, input from stdin is also echoed. The intended use of this is when input is piped to ft. clock returns the accumulated elapsed cpu time in milliseconds. prop n fmla the formula fmla is translated into a propositional formula in a domain with n elements and the propositional decision procedure is applied. trans n fmla the formula fmla is translated into a propositional formula in a domain with n elements and written out in a form that can be read by ft. If the formula written out by trans n fmla is read by ft, it will be given an internal representation identical to that used when prop n fmla is input. stack [n] stack alone gives the current size of the main stack. With an argument, the stack is resized to n bytes. fstack [n] similar to stack, for the formula stack. System variables ================ If the name of a system variable is input, the current value of that variable is written out. The system variables and their default values are given below. (P) indicates that the variable applies only to propositional input. (This is chiefly due to sheer laziness.) (D) means that the variable is relevant only for non-propositional input, i.e. formulas containing quantifiers or free variables. ucon 1 Default initial contraction value for universal formulas (D) icon 1 Default initial contraction value for implications (D) iffcon 1 Default initial contraction value for equivalences (D) ustep 1 Universal contraction parameter increment (D) istep 1 Implication contraction parameter increment (D) iffstep 1 Equivalence contraction parameter increment (D) allall 1 If true, allall compaction is performed (D) allimp 1 If true, allimp compaction is performed (D) alliff 1 If true, alliff compaction is performed (D) someor 1 If true, someor compaction is performed (D) somesome 1 If true, somesome compaction is performed (D) oror 1 If true, oror compaction is performed orsome 1 If true, orsome compaction is performed (D) orlock 1 If true, or-locking is performed somelock 1 If true, existence-locking is performed (D) andgather 0 If true, and-gathering is performed (P) orgather 0 If true, or-gathering is performed (P) anduse 1 If true, and-use-checking is performed (P) oruse 1 If true, or-use-checking is performed (P) allinv 0 If true, assumed all-invertibility is active (D) ifftrans 0 If true, formulas are expanded to eliminate equivalence timeout 0 If >0, maximum time in real seconds to spend on a problem forever 0 If true, contraction deepening is active echo 1 If true, input from files is echoed. If 2, echo stdin, too. tellme 6 See below syntax 0 If true, only a syntax check is performed eq 0 If true, transfer checking is done by address (P) minimal 0 If true, proofs in minimal logic are sought (P) topsift 1 If true, solutions are sifted at top level (D) twosift 1 If true, two-premiss sifting is performed (D) stuse 0 If true, stack usage is reported szsave 1000 The size of save stacks, in longs. (D) implock 1 If true, implication locking is active (D) pcheck 0 If true, perform prop checking. Several of these variables represent optimizations essential to the performance of the algorithm. They are included as switches only for the purpose of documenting the importance of these optimizations (if the theorem prover is to be able to do anything at all). This applies to the compaction variables allall, allimp, alliff, oror, orsome, and to anduse, oruse, twosift, implock. tellme is a bit flag: if bit 0 is true, a dot is printed for each solution skipped at top level. If bit 1 is true the number of such solutions is reported. If bit 2 is true, a colon is printed whenever a solution cannot be saved because of lack of space on the save stack of the sequent. If bit 3 is true, a semicolon is printed whenever twoold() returns true, i.e. whenever a solution of the left premiss in a two-premiss rule is rejected because of two-premiss sifting. The variables anduse and minimal are coupled: if minimal is set to true, anduse is set to false; if anduse is set to true, minimal is set to false. A note on szsave: there is a safety margin of 100 longs when terms are copied to the save stacks. This means that using terms requiring more than 100 longs of storage in conjunction with internal sifting may lead to a crash. allinv differs from the other variables in representing an "optimization" which makes the algorithm incomplete. For example, with allinv true, the following is unprovable: p1&Ax(p1->p2|q)&Ax(p2->p3|q)&Ax(p3->q)->q. The intended use of allinv is only to check whether a particular horrible result or non-result is due to the algorithm trying out endless permutations of universal formulas. If ft is compiled with DEBUG defined in the file ft.h, a variable "trace" is available. If trace is true, some (probably useless) information is written out during execution of the proof algorithm. Also, with DEBUG defined, the answer "Y" is accepted to the question "More? (y/n)" and interpreted as "y" with the side effect of setting trace to 1. If trace is 2, more information is written out. If bit 1 is set in the debugging variable dflag, Y will set trace to 2, otherwise to 1. If bit 0 is set in dflag, a quit signal (^\) will cause tracing to begin. If bit 2 is set in dflag, bindings will not be printed after a unification of an atomic input s=t. Formulas ======== Input that does not begin with quit, set, reset, read, clock, prop, trans, stack, or fstack, and is not the name of a system variable is assumed to be a formula to be proved. If the variable syntax is true, however, only the parsing of the formula is carried out. Problems can only be input as formulas to be proved; however, comments and whitespace can be used to present problems in a readable form. For example [1] AxAy(p(x)&q(y)->r(x)) & [2] AxAy(r(x)->p(x)&q(y)) & [3] Ex(p(x)|r(x)) & [4] Ax(q(x)|~q(x)) -> % Conclusion first established in 1937 [5] Ex(p(x)&~q(x)) | Axq(x). Formulas are written using the following syntax: Connectives are & (conjunction), | (disjunction), -> (implication), <-> (equivalence), ~ (negation). The order of precedence is ~ & | -> <-> where each connective binds harder (i.e. has lower precedence in Prolog's sense) than those on its right. All the binary connectives are right-associative. Thus e.g. p | q & r -> s <-> t <-> u is to be read as ((p | (q&r)) ->s) <-> (t <-> u). A function symbol or predicate symbol consists of a string of lower case letters followed by an optional string of digits. This includes zero-place function symbols (individual constants) and zero-place predicate symbols (propositional symbols). Quantifiers are A (universal quantifier) and E (existential quantifier). A bound variable consists of one lower case letter followed by an optional string of digits. A free variable consists of one upper case letter other than A or E followed by an optional string of digits. Terms and atomic formulas are written in standard notation. Thus e.g. zog(a,banana(X)) is an atomic formula, and also a term, but not at the same time. ft applies a strict syntax check in the following sense: in one and the same formula, the categories function symbol, bound variable, and predicate symbol must be disjoint, and the arity of a function symbol or predicate symbol must be well-determined. Thus, for example, "zog" cannot be used in the same formula both as a predicate symbol and a function symbol, or as a binary and as a ternary function symbol. The identity symbol is accepted in formulas, written as usual as an infix operator. However, this is a bit of a fraud: identity logic is not incorporated in version 1.2 of ft, and s=t is treated like any other atomic formula, with one exception: if an atomic formula s=t is entered, a unification of s and t is attempted and failure or bindings returned. There is the following addition to the usual predicate logic syntax: The connectives ~, ->, and <-> and the universal quantifier A may be followed by an optional positive integer n indicating the maximal number of times that the formula may be used in a branch of an attempted proof (the contraction parameter). If such an annotation is present, it supersedes the default contraction settings given by ucon, icon, iffcon. PROVING FORMULAS ft will try to prove a formula using the current settings of the system variables. If the attempt succeeds, ft reports "yes" and the time in milliseconds spent on finding the proof. If the input formula contains free variables, ft reports the bindings of those variables for which a proof was found, after which the prompt "More? (y/n)" appears. An affirmative answer prompts ft to backtrack in the search for a proof of the input sequent and present any further answers found. If the variable topsift is true, solutions will be saved, and ft will only present solutions that are not instances of old solutions. How many redundant solutions there are at top level depends on whether twosift is true. By a harmless quirk in the print routines, variables will be printed with an initial * or an initial _ (followed by an integer). A case that is treated specially is that of an input formula not containing free variables or quantifiers. In this case a decision procedure for intuitionistic propositional logic is invoked. All contraction annotations are ignored. As stated previously, atomic input s=t is interpreted as a unification task, but otherwise there is no special treatment of identity. When the attempt to prove a formula fails, or when no more solutions can be found, ft will report failure and the time spent on the task, provided the variable forever has value 0. If forever has value 1, ft will increase the default contraction values in accordance with the values of the variables ustep, istep, and iffstep and try again. If the formula is unprovable, this process will go on indefinitely. There are only two exceptions: propositional formulas, and formulas in which all implications, equivalences, and universal formulas are annotated with a contraction parameter. In these cases, the value of forever is immaterial. There are two ways of stopping ft's attempt to prove a formula. The first is to stop the search for a proof with ^C. This will return ft to top level. The other way is to give a value to the variable timeout. This value is interpreted as an upper bound, in real seconds, on the time to be spent on any one problem. If the formula has not been disposed of within that time, ft reports a timeout and continues with the next input item (thus there is no return to top level in this case). ERROR MESSAGES Various internal errors that should not occur will cause ft to quit with an explanatory message. There is also the theoretical possibility of unexplained errors indistinguishable from bugs, since for reasons of efficiency not every possible overflow situation is checked, although very many such checks are made. Errors in the input will prompt the response "syntax error" or "inconsistent syntax", with an indication of where the trouble lies. The error messages "main stack overflow" and "formula stack overflow" cause a return to top level and can only be dealt with by increasing the size of the stack or formula stack using the commands stack, fstack. The current reclaiming of stack space is efficient enough to make these messages rare. "Auxiliary stack overflow" should never happen. "Memory allocation error" means that it was not possible to obtain more memory from the operating system (for the main stack, the formula stack, or the individual save stacks used in a proof). There are some other possible non-disastrous errors, such as read stack overflow or bad numerical values. DIFFERENCES BETWEEN 1.1 AND 1.2 The chief difference is that an awful bug in the treatment of disjunction on the left in the propositional algorithm has been fixed, with the consequence that a few propositional test cases run a great deal more slowly. A gap in the syntax analysis, whereby Ax(p(x)&x) was admitted, has been eliminated. DIFFERENCES BETWEEN 1.2 and 1.21 A "long" has been changed to "int" in the definition of sysvars[], and some prototyping corrected. DIFFERENCES BETWEEN 1.21 and 1.22 A bug in the routine textractvars() in sift.c has been fixed. DIFFERENCES BETWEEN 1.22 and 1.23 The propcheck variable is now just a boolean. A variable has been made local.