Run-time Optimisations for Reasoning with Intensional Logics.
Allan M. Ramsay · 2000
. Most optimisation techniques for theorem provers for first-order logic rely on static analysis of the problem statement. For intensional logics, such as static analysis cannot be relied on, since it is impossible to predict what literals may be introduced by the intensional rules. The current paper shows how to use a dynamic (run-time) version of one well-known static optimisation, and considers its relationship to the use of `relevance checking' in Satchmo. 1 A constructive intensional logic We have shown elsewhere [8, 3] how to extend [6]'s theorem prover Satchmo to cope with [9]'s property theory. Property theory is a highly intensional logic which, roughly speaking, allows you to perform unconstrained quantification over propositions and properties, but places constraints on the conditions under which the Tarski biconditional (xP ):t $ P t=x holds. This language has numerous potential applications: I use it primarily for reasoning about natural language semantics, becaus...