I'm trying to use the Kowalski graph algorithm for resolution theorem proving. The description of the algorithm at http://www.doc.ic.ac.uk/~rak/ is silent on what to do about the large number of duplicate clauses it generates. I'm wondering if there's a well-known technique for dealing with them? In particular, you can't simply suppress...
I have a set of A's and a set of B's, each with an associated numerical priority, where each A may match some or all B's and vice versa, and my main loop basically consists of: Take the best A and B in priority order, and do stuff with A and B. The most obvious way to do this is with a single priority queue of (A,B) pairs, but if there...
I'm carrying out some experiments in theorem proving with combinator logic, which is looking promising, but there's one stumbling block: it has been pointed out that in combinator logic it is true that e.g. I = SKK but this is not a theorem, it has to be added as an axiom. Does anyone know of a complete list of the axioms that need to be...
Hi all, I'm hoping to pick one of the many assisted theorem provers (rather than automatic ones) but there are rather a lot to choose from! Does anyone have any you prefer and may I ask why? Thanks! ...
The documentation says that REWRITE_TAC; "Rewrites a goal including built-in tautologies in the list of rewrites." where SIMP_TAC ; Rewrites a goal including built-in tautologies in the list of rewrites. These look like they do the same thing to me but appear to have different effects. Any ideas? ...
I'm trying to prove a simple lemma in Agda, which I think is true. If a vector has more than two elements, taking its head following taking the init is the same as taking its head immediately. I have formulated it as follows: lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l))) -> head (init xs) ≡ head xs lem-headIn...
I've heard a bit about using automated theorem provers in attempts to show that security vulnerabilities don't exist in a software system. In general this is fiendishly hard to do. My question is has anyone done work on using similar tools to /find/ vulnerabilities in existing or proposed systems? Eidt: I'm NOT asking about proving ...
Summary: if we are trying to use combinator logic to solve first-order logic type problems, is the best method to feed in free variables and use the standard first-order unification algorithm? In standard first-order logic, consider the problem of deducing that the following is a contradiction p(x) ~p(5) By the rule that we can subst...