This is a rule that guides [A] or [A or B] from a propsition [A and B]. When writing such as LOGIC (a1, a2, a3), its arguments a1, a2, a3 are already demonstrated (registered in a formula table, udirect) labels of formulas. Computers take those formulas' logical products and make them into formulas of assumption and compound a new formula that makes wanted formula as a conclusion formula, making sure that it will always be right by creating a true value table that has 2³=8 columns concerning variables A,B,and C. For example, when it is a1 : A, a2 : f(x), a3 : A or f(x) imp B,
are correct inference; however, this is made sure by the system as shown below.
A f(x) B A and f(x) and (A or f(x)imp B) imp B
0 0 0 0 1 0 0 0 1 0 1 1 0 1 0 0 1 0 0 1 1 0 1 1 1 0 0 0 1 0 1 0 1 0 1 1 1 1 0 0 1 0 1 1 1 1 1 1
Therefore, because under imp are all 1, this formula will be constantly true; so, this inference is correct.
Sometimes, LOGIC does not have arguments. In that case, the conclusion formula itself is constantly correct.
Also, formulas such as (All x) (f(x) and b) or [a=b or c] are considered as one variable (f(x) or b are not viewed as variables and parts that were quantitized are considered as one variable).