marisakirisame / first_order_logic_prover Goto Github PK

since the function explore a subtree until it terminate, and one of the subtree can be undecidable while the main tree is decidable(on correct code), this create unnecessary unhalted situation.

😖想试用一下，然而找不到栗子（其实要有个文档更好了，感兴趣的人嘛

There are too many codes which do almost the same thing with propositional_calculus_proofer. For example, both of them do propositional calculus. This means a GREAT refractor, possibly one that will effect all the code( sound a lot of work but sadly is a must QAQ )

use boost::mpl

Currently it's eating me 3.5GB of memory and 3 minutes of time. Reduce it.

also x/\x/!x

Praser -> Parser

static_assert( std::is_convertible< or_and_or_not_type, negation_in_type >::value, "should be convertible" );

compiling is too slow in C++

For example, free_prop_sentence::move_quantifier_out will introduce two quantifier.

make branching share the same base sequent->that is, deducting sequent in base deduction tree effect the other tree derived from the same sequent.

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.

Don't know how to integrate it with get_cnf... Need some thought.

On my machine the unit test failed:
Running 5 test cases...
unknown location(0): fatal error in "gentzen_system_test": std::exception: boost::bad_get: failed value get using boost::get
unknown location(0): fatal error in "resolution_test": std::exception: boost::bad_get: failed value get using boost::get
../first_order_logic_prover/test.hpp(140): last checkpoint

*** 2 failures detected in test suite "Master Test Suite"
Press to close this window...

Fucking waste three hour debugging bug from boost::optional implicit conversion.

sometimes CNF are better stored in set and sometimes list. Resolve this by making some functor argument for to_CNF

return a ome enum form to entail more meaning

Do not know what to do when one type cannot be converted to other type. Please comment if anyone knows.