theorem_prover/example.hpp at master · llhhbc/theorem_prover · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
#ifndef THEOREM_PROVER_EXAMPLE
#define THEOREM_PROVER_EXAMPLE
#include "propositional_logic/proposition.hpp"
#include "first_order_logic/first_order_logic.hpp"
#include "propositional_logic/resolution_method.hpp"
#include "first_order_logic/praser.hpp"
namespace theorem_prover
{
	void propositional_logic_test( )
	{
		using namespace propositional_logic;
		std::shared_ptr< proposition > A( new proposition( "A" ) );
		std::shared_ptr< proposition > B( new proposition( "B" ) );
		std::shared_ptr< proposition > C( new proposition( "C" ) );
		std::shared_ptr< proposition > not_a( proposition::make_not( A ) );
		std::shared_ptr< proposition > valid_prop( proposition::make_or( A, not_a ) );
		std::shared_ptr< proposition > unsatisfiable_prop( proposition::make_and( A, not_a ) );
		std::shared_ptr< proposition > associativity_law_prop(
					proposition::make_equal(
						proposition::make_or(
							proposition::make_or( A, B ),
							C ),
						proposition::make_or(
							proposition::make_or( B, C ),
							A ) ) );
		std::shared_ptr< proposition > valid_prop2( proposition::make_imply( A, proposition::make_imply( B, A ) ) );
		auto res1 = A->get_satisfiability( );
		auto res2 = valid_prop->get_satisfiability( );
		auto res3 = unsatisfiable_prop->get_satisfiability( );
		auto cnf = to_CNF( unsatisfiable_prop );
		auto cnf2 = to_CNF( proposition::make_not( associativity_law_prop ) );
		auto cnf3 = to_CNF( associativity_law_prop );
		assert(
					res1 == satisfiable &&
					res2 == valid &&
					res3 == unsatisfiable &&
					associativity_law_prop->get_satisfiability( ) == valid &&
					valid_prop2->get_satisfiability( ) == valid &&
					is_unsatisfiable( cnf ) && is_unsatisfiable( cnf2 ) && ! is_unsatisfiable( cnf3 ) );
	}

	void first_order_logic_test( )
	{
		using namespace first_order_logic;
		auto fol = make_imply(
								 make_all( "x", make_predicate( "F", { make_variable( "x" ) } ) ),
								 make_all( "x", make_predicate( "F", { make_function( "f", { make_variable( "x" ) } ) } ) ) );
		auto fol2 = make_imply(
									make_some(
										"x",
										make_imply(
											make_variable( "p" ),
											make_function( "Q", { make_variable( "x" ) } )
											) ),
									make_imply(
										make_variable( "p" ),
										make_some(
											"z",
											make_function( "Q", { make_variable( "z" ) } ) ) )
									);
		auto fol3 = make_imply(
									make_and(
										make_all(
											"x",
											make_function( "P", { make_variable( "x" ) } ) ),
										make_some(
											"y",
											make_function( "Q", { make_variable( "y" ) } ) ) ),
									make_and(
										make_function(
											"P",
											{ make_function( "F",  { make_variable( "v" ) } ) } ),
										make_some(
											"z",
											make_function( "Q", { make_variable( "z" ) } ) ) ) );
		auto fol4 = make_imply(
									make_and(
										make_function( "p", { make_variable( "x" ) } ),
											make_equal( make_function( "f", { make_variable( "x" ) } ), make_variable( "x" ) ) ),
									make_function( "p", { make_function( "f", { make_variable( "x" ) } ) } ) );
		assert( ( fol->is_valid( ) ) && fol2->is_valid( ) && fol3->is_valid( ) && fol4->is_valid( ) );
	}

	int example( )
	{
		first_order_logic_test( );
		return 0;
	}

}
#endif //THEOREM_PROVER_EXAMPLE