Lesson 01

How a rule becomes a checkable problem

What must we write down before a program can check a claim?

A reasoning system cannot check an intention. It needs a formal claim, the rules that give its symbols meaning, and a stated form of evidence.

After this lesson, you should be able to

Distinguish a claim, a constraint, and a decision problem.
Explain why a successful check applies to a formalization rather than automatically to its source prose.
Identify the evidence and trusted computing base for a small reasoning task.

1.1

Start with the statement that will be checked

Suppose a course requires at least three completed mathematics classes. The ordinary sentence gives a person enough context to apply the rule, but software still needs several choices fixed. What counts as a mathematics class? Does a course in progress count? Is the number three inclusive? A formalization answers those questions.

One possible formal statement is completed_math_courses ≥ 3. The variable records a nonnegative integer, and the comparison includes three. The program can now evaluate the rule for a supplied record. Its answer applies to this formal statement and to the data given to it.

1.2

Constraints define the permitted cases

A constraint restricts which values are allowed. Several constraints form one problem only after their relationship is clear. If every constraint must hold, the problem uses conjunction. If one of several alternatives is enough, it uses disjunction.

A decision problem asks for an outcome such as yes or no. A search problem asks for a value that meets the constraints. Solvers often do both: they report sat and return a model containing the values they found.

1.3

Evidence depends on the result

A model can establish that constraints are satisfiable because another procedure can substitute the values and evaluate every rule. Unsat requires a different argument. One failed assignment says only that one choice did not work, so an unsat result needs a certificate, an exhaustive argument, or another sound decision route.

The checker, formal language, and primitive assumptions form part of the trusted computing base. Reducing that base can make review easier, but a small checker still has to implement the right rules.

Worked example

Check a course-eligibility rule

A student may enroll when they have completed at least three mathematics classes and have no schedule conflict. Maya has completed four classes and has a conflict.

Formalize
Let m be the completed course count and c mean that a conflict exists. The rule is (m ≥ 3) and not c.
Assign
Maya's record gives m = 4 and c = true.
Evaluate
The first constraint is true. The second is false because not true is false. Their conjunction is false.
State the boundary
The result checks the encoded rule and supplied record. It does not establish that the record is accurate or that the written policy was encoded correctly.

Result. Maya does not satisfy this formalized rule because the schedule constraint fails.

1.4

Check your understanding

Answer each question before opening the explanation.

1 Why does one satisfying model establish sat, while one failed model does not establish unsat?

Sat means that at least one model works. Unsat means that none work, so rejecting one assignment leaves every other assignment open.

2 What remains unchecked when a program correctly evaluates a formalized policy?

The check does not establish that the formalization matches the policy or that the input record is complete and accurate.

Concept wiki

Terms in this lesson

All concepts