This program demonstrates a core proof to illustrate the soundness of an arbitrary elimination rule. While it does not support all formula types, the program still effectively conveys the proof's essence. Simply follow the instructions in the given order to use it effectively.
Set the Size of Agents
Firstly, determine the number of agents for your scenario. Note that there are only 9 predefined colors, so having up to 9 agents is advisable.
Select Agent's Followers
Secondly, define the social network among agents.
Select an agent:
Select its followers:
Set the Size of Prop
Thirdly, decide on the number of explicit propositional variables in your scenario. A range of 3 to 5 is recommended.
Explicit Prop :
Explicit variables are the sole variables occur in the formulas being tested.
Implicit Prop:
Implicit variables may appear in arbitrary announcements but are not occur in the formulas.
Augment:
Augmentation abstracts the concept of infinite variables in Propositional Variables, indicating that new variables not occur in formulas can always be found, both explicitly and implicitly. This property is known as "non-cofiniteness" or "non-greediness."
Assign beliefs:
Fourthly, after defining agents and propositional variables, click the button below to generate a background for assigning beliefs to agents.
Fifthly, to assign beliefs, click on a node. A dropdown list will appear for you to select agents. Press "Enter" to confirm your choices. Hold "Ctrl" to select multiple agents. To illustrate the proof correctly, avoid clicking "Expand Graph" or "dispel w" initially.
Sixthly, input a formula below to test its satisfiability within the defined model. The formula should follow the format [i:θ]φ, where 'i' represents an agent, 'θ' can include any combination of implicit and explicit variables, and 'φ' should only contain implicit variables within announcements.
Enter Your Formula
Result:
Enter Message
Seventhly, with your formula still in the input box, click "Expand Graph" and then "dispel w". Next, enter 'θ' in the box below. If 'θ' contains implicit variables, replace each with its successor (e.g., change (p&~x) to (p&~y)), and then click "Preserve Arbitrariness."
Finally, return to the "Enter Your Formula" section. Replace 'θ' with 'w' in the input box, and in 'φ', substitute each implicit variable with its successor. Note that 'w' will not occur in 'φ'. Check the satisfiability again; it should remain consistent.