Check why algorithm doesn't halt for certain input

ixjf / logic-rs

A parser of relational predicate logic & truth tree solver, written in Rust.

https://ixjf.github.io/logic-rs/

MIT License

16 stars 1 forks source link

Check why algorithm doesn't halt for certain input #21

Open ixjf opened 5 years ago

ixjf commented 5 years ago

∀x∀y(R²xy ⊃ ~R²yx)
∴ ~∀x∀y(R²xy ⊃ R²yx)

∀x((P¹x & B¹x) ⊃ ∀y((P¹y & O¹y) ⊃ H²xy)),
P¹e
∴ ∀x((P¹x & B¹x) ⊃ H²xe)

(∀x)(S¹x ⊃ (∀y)(A¹y ⊃ (∀z)(T¹z ⊃ (S³xyz ⊃ ~F²xz))))                                                    
∴ (∀x)(∀z)((S¹x & ((∃y)(A¹y & T¹z & S³xyz))) ⊃ ~F²xz)

∀x(A ⊃ B)