I am working on building a toy automated theorem prover,

What I want to do is to efficiently generate sentences in peano arithmetic, that I can attempt to verify as True/False/requires-more-resources in a higher model of logic.

My first task I want to work on is to build a tool that can list out statements in PA

So my current idea was to build a compiler that can recognize, if a sentence is a well formed sentence in PA, and then brute force all possible strings in lexical order,

$$\forall, \forall \exists , \forall x, \forall |, ... (\forall x|\exists y...), ... $$

And have the compiler recognize if this is a sentence or not, but the problem is that it will end up spending a lot of time shifting through junk.

Since most permutations of character simply aren't meaningful at all,

Is there a more efficient way for me to list out sentences? perhaps a way to compute the first $n$ sentences in $O(n^2)$ time and $O(n^2)$ space (that would have to be asymptotically optimal).

Even better is if this procedure can be a start stop procedure, that is it can be given a most recently generated sentence $T_n$, and automatically form that point on, start generating additional sentences $T_{n+1}, ... $

  • 2
    $\begingroup$ This is an instance of a more general problem. If you take formulas and not sentences, then you can write the language out as a BNF, which is a special case of a Context Free Grammar. Then an answer to your question can be found here: stackoverflow.com/questions/17387686/… $\endgroup$ – cody Jul 29 '16 at 12:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.