Tableau Proof Assistant

Formulas of ASAL:

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 Proof Assistant

Formulas of ASAL:

Tableau Rules

Tableau Output

Closure Condition

Model