Literal Belief formula: Baθ or ~Baθ where a is an element of Agents and θ is an element of Prop.
Conjunction: Use the ampersand symbol & between two formulas. E.g., (φ&ψ) where both φ and ψ are formulas.
Disjunction: Use the plus symbol + between two formulas. E.g., (φ+ψ).
Free Announcement: Use the symbol [a:θ] before the formula. E.g., [a:θ]φ.
Diamond Sincere Announcement: Use the symbol <a!θ> before the formula. E.g., <a!θ>φ.
Box Sincere Announcement: Use the symbol [a!θ] before the formula. E.g., [a!θ]φ.
Diamond Arbitrary Announcement: Use the symbol <a!> before the formula. E.g., <a!> φ.
Box Arbitrary Announcement: Use the symbol [a!] before the formula. E.g., [a!]φ.
Brackets: Every formula connected by a binary operator should be enclosed within a pair of brackets. E.g., (φ+ψ), not φ+ψ.
Tableau Rules
[:]∨ [b:γ]...[c:χ](φ∨ψ)
[b:γ]...[c:χ]φ
[b:γ]...[c:χ]ψ
[:]∧ [b:γ]...[c:χ](φ∧ψ)
[b:γ]...[c:χ]φ
[b:γ]...[c:χ]ψ
[:]K [b:γ]...[c:χ][a:θ]Bdε
[b:γ]...[c:χ]Bdε
[b:γ]...[c:χ]Bd(θ>ε)
dFa
[:]~K [b:γ]...[c:χ][a:θ]~Bdε
[b:γ]...[c:χ]~Bd(θ>ε)
[b:γ]...[c:χ]~Bdε
~dFa
<!θ> [b:γ]...[c:χ]<a!θ>φ
[b:γ]...[c:χ]Baθ
[b:γ]...[c:χ][a:θ]φ
[!θ] [b:γ]...[c:χ][a!θ]φ
[b:γ]...[c:χ]~Baθ
[b:γ]...[c:χ][a:θ]φ
<!> [b:γ]...[c:χ]<a!>φ
[b:γ]...[c:χ]<a!p>φ
[!] [b:γ]...[c:χ][a!]φ
[b:γ]...[c:χ][a!θ]φ
where [b:γ]...[c:χ] is either a sequence of free announcement operators or empty and p is a new atomic message which does not occur in any ancestor.
Due to my fault, currently agents should be only denoted by one letter from a to e. And propositional variable should be from p to z. Do not use a_1, b_2, p_1, x_2 and etc..
Tableau Output
Expand the tableau by double clicking compound formula. Or do it automatically except arbitrary formulas.
Closure Condition
A branch is closed if it contains a formula ~Baθ such that θ is a
tautology, or, in addition, formulas Baθ1, ...Baθn such that (θ1 & ... & θn > θ)
is a tautology.
A branch is closed if it contains both bFa and ~bFa.
Model
Please choose an open branch when prompted, selecting from left to right. Opting for a closed branch to create a model is not advisable.