I am deeply interested in this project. I have some newbie questions :)

[enjoysmath]

1. What source book, article, etc did you use to figure out how to code this?
2. How does your resolution algorithm work?
3. How does your proof checking algorithm work?
4. Would you be interested in working on a project together that involves diagram chase-style proofs?

Just a brief overview in your answers is fine.

5. Does the library have any memory leaks or with this algorithm area, or was it easy to rule out the possibility of those?
6. Did you use OOP? When you create the objects such as ForAll, Prop, etc during runtime, are they created in a std::vector<Assertion*> stl structure, or what?
7. Have you figured out how to convert to prenex-normal form?

In my application, at some point I will covert to prenex-normal form or even Skolem form, so that I can hash the formulas! That would mean near O(1) lookup time to see if P(x,y,z) matches Q in Q(x,y,z) => R(x,y,z) a theorem. You handle the variable matching via standardizing them from left-to-right with format indices %0, %1, %2, ...

so "forall a in A, f(a) in B" goes to "forall {0} in {1}, {2}({0}) in {3}". Now you have a standard form for the formulas!

Constants in a formula go through unchanged. You store the association in map<int, Variable> so that you can for example determine a theorem's conclusion in the users chosen variable alphabet.

Anyhow. As you can see, I really dig this project/type of project.

[MarisaKirisame]

Sorry! I missed the issue!

What source book, article, etc did you use to figure out how to code this?

I think stuff from here is from , and . additionally is a good book even though I had not read it when coding it up.

How does your resolution algorithm work?

It is just like any other resolution algorithm

How does your proof checking algorithm work?

It search for a proof tree deviation in gentzen's sequent calculus, see

Would you be interested in working on a project together that involves diagram chase-style proofs?

Sorry, I am busy with other stuff.

Does the library have any memory leaks or with this algorithm area, or was it easy to rule out the possibility of those?

not that I know of.

Did you use OOP? When you create the objects such as ForAll, Prop, etc during runtime, are they created in a
std::vector<Assertion*> stl structure, or what?

Read up on Algebraic Data Type, the canonical method to do this kind of things.

Have you figured out how to convert to prenex-normal form?

Yes, it is written in the books. It is not much different from e.g. using De Morgan Law to get CNF.