Model Generator

Set the Size of Agents

Select Agent's Followers

Select an agent:

Select its followers:

Set the Size of Prop

How to write correct messages of belief:

Propositional Variables: Use elements in Prop.
Negation: Use the tilde symbol ~ before the propositional variable or message. E.g., ~p.
Conjunction: Use the ampersand symbol & between two messages. E.g., (p&q).
Disjunction: Use the plus symbol + between two messages. E.g., (p+q).
Implication: Use the greater than symbol > between two messages. E.g., (p>q).
Brackets: Every message connected by a binary operator should be enclosed within a pair of brackets. E.g., (p&q), not p&q.

Select an Agent for Belief Assignment:

Input the Belief Message:

Agent Beliefs:

Announcements are in form of [a:p], which means a announces p to its followers. After you update model, you may try to click Draw Graph again.

How to Write Well-formed Formulas:

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., (φ+ψ).
Implication: Use the greater than symbol > between two formulas. E.g., (φ>ψ).
Free 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 φ+ψ.

Enter Your Formula

Result:

Axiom System Fsal

An axiom system is a set of foundational truths (axioms) used to derive further theorems through logical reasoning. In such a system:

Axioms are basic, accepted truths.
Theorems are derived statements proven using axioms and inference rules.
Rules of Inference dictate the valid ways of deriving new theorems.

The following system \( \mathsf{Fsal} \) is sound and complete, meaning every theorem is valid and then satisfied by any model within this system, and only theorems are valid.

Our original model is defined with infinite propositional variables but here we only employ a finite number of variables. To test a formula by the satisfiability checker above, ensure it is well-formed, using only the defined propositional variables in \( Prop \) and agents.

Definition:

Let \( \mathsf{Fsal} \) be the formal system which is a set of all valid formulas of \( L_{FSAL} \). Say a formula is a theorem of \( \mathsf{Fsal} \) if it is a consequence of the following axioms and rules:

Axioms:
[Taut] All substitution instances of propositional tautologies
[K_⊤] \( B_{i}\theta \) where \( \theta \) is an instance of propositional tautology.
[K_B] \( B_{a}(\theta \rightarrow \gamma) \rightarrow (B_{a}\theta \rightarrow B_{a}\gamma) \)
[K_[:]] \( [a:\theta](\phi \rightarrow \psi) \rightarrow ([a:\theta]\phi \rightarrow [a:\theta]\psi) \)
[[:]-Dual] \( \neg [a:\theta]\phi \leftrightarrow [a:\theta]\neg\phi \)
[Comm] \( [a:\gamma][b:\theta]\phi \leftrightarrow [b:\theta][a:\gamma]\phi \)
[UMon] \( B_{b}\chi\rightarrow[a:\theta]B_{b}\chi \)
[SDMon] \( [a:\theta]B_{b}\chi\rightarrow B_{b}(\theta\rightarrow\chi) \)
[RDMon] \( [a:\gamma]\neg B_{b}\gamma\rightarrow([a:\theta]B_{b}\chi\rightarrow B_{b}\chi) \)

Rules:
[MP] From \( (\phi \rightarrow \psi), \phi \), infer \( \psi \)
[[:]-Nec] From \( \vdash\phi \), infer \( \vdash[a:\theta]\phi \)

you may test the following instances with any model you defined

[Taut] (Bap + ~Bap)
[K_⊤] Ba(p+~p)
[K_B] (Ba(p>q)>(Bap>Baq))
[K_[:]] [a:q](Bbq>Bcp) > ([a:q]Bbq>[a:q]Bcp))
[UMon] (Bbp>[a:q]Bbp)
[SDMon] ([a:p]Bbq > Bb(p > q))
[RDMon] ([a:r]~Bbr > ([a:p]Bbq> Bbq))