Enter a formula of standard propositional, predicate, or modal logic. The page will try to find either a countermodel or atree proof (a.k.a. semantic tableau).
Examples (click!):
To enter logic symbols, use the buttons above the text field, or type~ for¬,& for∧,v for∨,-> for→,<-> for↔,! for∀,? for∃,[] for□,<> for◇. You can also use LaTeX commands.
If you want to test an argument with premises and conclusion, use|= to separate the premises from the conclusion, and use commas to separate the premises. See the last example in the list above.
Any alphabetic character is allowed as a propositional constant, predicate, individual constant, or variable. Numeral digits can be used either as singular terms or as indices (as inFx1), but don't mix the two uses. '+', '*', and '-' can be used as function expressions. Predicates (except identity) and function terms must be in prefix notation. Function terms must have their arguments enclosed in brackets. SoF2x17,Rab,R(a,b),Raf(b),F(+(1,2)) are ok, but notAnimal(Fred),aRb, orF(1+2). (In fact, these are also ok, but they won't be parsed as you might expect.) The order of precedence among connectives is¬, ∧, ∨, →, ↔. Association is to the right. Quantifier symbols in sequences of quantifiers must not be omitted: write∀x∀yRxy instead of∀xyRxy.
Besides classical propositional logic and first-order predicate logic (with functions and identity), a few normal modal logics are supported. If you enter a modal formula, you will see a choice of how the accessibility relation should be constrained. For modal predicate logic, constant domains and rigid terms are assumed.
The source ison github.
Comments, bug reports and suggestions are always welcome: