Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- copy(A, B, Proof) :- %If all true, copy rule is true.
- A < B, %Row copied to is higher than row copied from.
- get_rule(B, Proof, Rule), %Get rule of row copied to.
- Rule = copy(A), %Check that the rule is equal to copy of row A.
- get_prop(A, Proof, PropA), %Get proposition of row being copied from.
- get_prop(B, Proof, PropB), %Get proposition of row being copied to.
- PropA = PropB. %Are the proposition of the rows equal to each other.
- %__ADD FUNCTIONALLITY OF BOXES__
- andint(A, B, C, Proof) :- %If all true, copy rule is true.
- A < C, %Left conjunction cannot be on a row after the row with the andint rule.
- B < C, %Right conjunction cannot be on a row after the row with the andint rule.
- get_rule(C, Proof, Rule), %Get rule of row being introducted an and.
- Rule = andint(A, B), %Check that the rule is equal to andint of row A and B.
- get_prop(A, Proof, PropA), %Get proposition of row being andint:ed from on the left conjunction.
- get_prop(B, Proof, PropB), %Get proposition of row being andint:ed from on the right conjunction.
- get_prop(C, Proof, PropC), %Get proposition of row being andint:ed to.
- and(PropA, PropB) = PropC. %Check that the and of PropA and PropB is the same as PropC.
- andel1(A, B, Proof) :- %If all true, andel1 rule is true.
- A < B, %Row copied to is higher than row copied from.
- get_rule(B, Proof, Rule), %Get rule of row copied to.
- Rule = andel1(A), %Check that the rule is equal to andel1 of row A.
- get_prop(A, Proof, PropA), %Get proposition of row being copied from.
- get_prop(B, Proof, PropB), %Get proposition of row being copied to.
- get_pred_of_prop(PropA, PredA), %Get predicate of row being andel1:ed from.
- get_pred_l(PredA, PredLeftA), %Get the left conjunction of the predicate (left predicate).
- PredLeftA = PropB. %Check that the left predicate of the conjunction is the same as the prop of PropB
- andel2(A, B, Proof) :- %If all true, andel2 rule is true.
- A < B, %Row copied to is higher than row copied from.
- get_rule(B, Proof, Rule), %Get rule of row copied to.
- Rule = andel2(A), %Check that the rule is equal to andel2 of row A.
- get_prop(A, Proof, PropA), %Get proposition of row being copied from.
- get_prop(B, Proof, PropB), %Get proposition of row being copied to.
- get_pred_of_prop(PropA, PredA), %Get predicate of row being andel1:ed from.
- get_pred_r(PredA, PredRightA), %Get the right conjunction of the predicate (right predicate).
- PredRightA = PropB. %Check that the right predicate of the conjunction is the same as the prop of PropB
- orint1(A, B, C, Proof) :- %If all true, andel2 rule is true.
- A < C, %Row copied to is higher than row copied from.
- B < C,
- get_rule(C, Proof, Rule), %Get rule of row copied to.
- Rule = orint1(A, B), %Check that the rule is equal to or of row A.
- get_prop(A, Proof, PropA), %Get proposition of row being copied from.
- get_prop(C, Proof, PropC), %Get proposition of row being copied to.
- get_pred_of_prop(PropC, PredC), %Get predicate of row being orint1:ed from.
- get_pred_l(PredC, PredLeftC), %Get the left conjunction of the predicate (right predicate).
- PredLeftC = PropA. %Check that the right predicate of the conjunction is the same as the prop of PropB
- orint2(A, B, C, Proof) :- %If all true, andel2 rule is true.
- A < C,
- B < C,
- %Row copied to is higher than row copied from.
- get_rule(C, Proof, Rule), %Get rule of row copied to.
- Rule = orint2(A, B), %Check that the rule is equal to or of row A.
- get_prop(B, Proof, PropB), %Get proposition of row being copied from.
- get_prop(C, Proof, PropC), %Get proposition of row being copied to.
- get_pred_of_prop(PropC, PredC), %Get predicate of row being orint1:ed from.
- get_pred_r(PredC, PredRightC), %Get the left conjunction of the predicate (right predicate).
- PredRightC = PropB. %Check that the right predicate of the conjunction is the same as the prop of PropB
- orel(X, A, B, C, D, E, Proof) :-
- A < B,
- C < D,
- B < E,
- D < E,
- X < E,
- get_rule(E, Proof, Rule),
- Rule = orel(X, A, B, C, D),
- get_prop(B, Proof, PropB),
- get_prop(D, Proof, PropD),
- PropB = PropD.
- %__ADD FUNCTIONALLITY OF BOXES__
- impint(A, B, C, Proof) :-
- A < B,
- A < C,
- B < C,
- get_rule(C, Proof, Rule),
- Rule = impint(A, B),
- get_prop(A, Proof, PropA),
- get_prop(B, Proof, PropB),
- get_prop(C, Proof, PropC),
- get_pred_of_prop(PropC, PredC),
- get_pred_l(PredC, PredLeftC),
- get_pred_r(PredC, PredRightC),
- PropA = PredLeftC,
- PropB = PredRightC.
- impel(A, B, C, Proof) :-
- A < C,
- B < C,
- get_rule(C, Proof, Rule),
- Rule = impel(A, B),
- get_prop(A, Proof, PropA),
- get_prop(B, Proof, PropB),
- get_prop(C, Proof, PropC),
- get_pred_of_prop(PropB, PredB),
- get_pred_l(PredB, PredLeftB),
- get_pred_r(PredB, PredRightB),
- PropA = PredLeftB,
- PropC = PredRightB.
- negint(A, B, C, Proof) :-
- A < B,
- A < C,
- B < C,
- get_rule(C, Proof, Rule),
- Rule = negint(A, B),
- get_prop(A, Proof, PropA),
- get_prop(B, Proof, PropB),
- get_prop(C, Proof, PropC),
- get_pred_of_prop(PropC, PredC),
- get_pred_l(PredC, PredLeftC),
- PropA = PredLeftC,
- PropB = cont.
- negel(A, B, C, Proof) :-
- A < C,
- B < C,
- get_rule(C, Proof, Rule),
- Rule = negel(A, B),
- get_prop(A, Proof, PropA),
- get_prop(B, Proof, PropB),
- get_prop(C, Proof, PropC),
- get_pred_of_prop(PropB, PredB),
- get_pred_l(PredB, PredLeftB),
- PropA = PredLeftB,
- PropC = cont.
- contel(A, B, Proof) :-
- A < B,
- get_rule(B, Proof, Rule),
- Rule = contel(A),
- get_prop(A, Proof, PropA),
- PropA = cont.
- negnegint(A, B, Proof) :-
- A < B,
- get_rule(B, Proof, Rule),
- Rule = negnegint(A),
- get_prop(A, Proof, PropA),
- get_prop(B, Proof, PropB),
- get_pred_of_prop(PropB, PredB),
- get_pred_l(PredB, PredLeftB),
- get_pred_of_prop(PredLeftB, PredBB),
- get_pred_l(PredBB, PredLeftBB),
- PropA = PredLeftBB.
- negnegel(A, B, Proof) :-
- A < B,
- get_rule(B, Proof, Rule),
- Rule = negnegel(A),
- get_prop(A, Proof, PropA),
- get_prop(B, Proof, PropB),
- get_pred_of_prop(PropA, PredA),
- get_pred_l(PredA, PredLeftA),
- get_pred_of_prop(PredLeftA, PredAA),
- get_pred_l(PredAA, PredLeftAA),
- PropB = PredLeftAA.
- mt(A, B, C, Proof) :-
- A < C,
- B < C,
- get_rule(C, Proof, Rule),
- Rule = mt(A, B),
- get_prop(A, Proof, PropA),
- get_prop(B, Proof, PropB),
- get_prop(C, Proof, PropC),
- get_pred_of_prop(PropA, PredA),
- get_pred_l(PredA, PredLeftA),
- get_pred_r(PredA, PredRightA),
- neg(PredLeftA) = PropC,
- neg(PredRightA) = PropB.
- pbc(A, B, C, Proof) :-
- A < B,
- B < C,
- get_rule(C, Proof, Rule),
- Rule = pcb(A, B),
- get_prop(A, Proof, PropA),
- get_prop(B, Proof, PropB),
- get_prop(C, Proof, PropC),
- get_pred_of_prop(PropA, PredA),
- get_pred_l(PredA, PredLeftA),
- neg(PredLeftA) = PropC,
- cont = PropB.
- lem(A, Proof) :-
- get_rule(A, Proof, Rule),
- Rule = lem,
- get_prop(A, Proof, PropA),
- get_pred_of_prop(PropA, PredA),
- get_pred_l(PredA, PredLeftA),
- get_pred_r(PredA, PredRightA),
- neg(PredLeftA) = PredRightA,
- PropA = and(PredLeftA, PredRightA).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement