Scheme alike theorem Prover powered by PHP

SchemeProver is the simple theorem prover. It is powered by PHP and uses the scheme syntax.
» Test your theorem now «.

the Robbery

  1. Each of the men A, B and C were on the day of Theft in the store, and no other had entered the store on the day.
  2. If A is guilty, he has exactly one Accomplice.
  3. If B is innocent, Also C is innocent.
  4. If exactly two are guilty, then A is one of a them.
  5. If C is innocent, B is innocent.

(∧
)

(∧
)

(∧
)

(∧
)

(∧
)

(∧
)

Symbole ⊤ ⊥ ¬ A A ∧ B A ∨ B A → B A ↔ B
Usage true false (! A) (& A B) (v A B) (-> A B) (<-> A B)
⊤ ⊥ (¬ A) (∧ A B) (∨ A B) (→ A B) (↔ A B)
(& A B C ...) (v A B C ...)
Symbole Usage
⊤ true
⊥ false
¬ A (! A)
A ∧ B (& A B)
A ∧ B ∧ C ∧ ... (& A B C ...)
A ∨ B (v A B)
A ∨ B ∨ C ∨ ... (v A B C ...)
A → B (-> A B)
A ↔ B (<-> A B)

Notice: Trying to access array offset on value of type null in /var/customers/webs/kanti/kanti/sub-schemeprover/index.php on line 59

Notice: Trying to access array offset on value of type null in /var/customers/webs/kanti/kanti/sub-schemeprover/index.php on line 64

Notice: Trying to access array offset on value of type null in /var/customers/webs/kanti/kanti/sub-schemeprover/index.php on line 64