Application provides interface and algorithms for deduction reasoning in two-valued predicate logic. It is based on non-clausal resolution. It implements developed DCF technique.
Application provides interface and algorithms for deduction reasoning in two-valued predicate logic. It is based on non-clausal resolution. It implements developed DCF technique. (en)