Lernkarten
What are the components of satisfiability checking? [3]
1. Quantifier-free logical formula
2. Solver
3. Satisfiability of the input formula
What is the problem of quantifier-free logical formula?
How to specify input into a formula?
What is the problem of the solver?
How to solve the formula?
What is the problem of the satisfiability of the input formula?
How to specify output of satisfiability
What is a logical systems?
Framework for inference and correct reasoning
What is syntax? [2]
1. Form of logical formulas with axioms and inference rules
2. Combination of atomic propositions or constraints using boolean operators (and, or, not)
What is semantic? [2]
1. Structure derives and gives meaning to logical formulas
2. Substitute truth values or type correct for propositions such that the formula evaluates to true
What is the problem of substitution?
Hard or even undecidable (non-linear integer arithmetic)
