Prepositional logic plays a central role in digital hardware, software engineering, artificial intelligence, and areas of computer science where it is used to model systems, conditions, and properties. A variety of problems and systems can be modeled using prepositional logic, including practical problems in diagnosis, planning, scheduling, and the like. Analysis of systems modeled in prepositional logic and reasoning about their properties is then performed using standard techniques from prepositional logic. It is common to translate the system model into a standard form called the "conjunctive normal form" (CNF). The most important fundamental technique in propositional logic is that of checking whether a given formula in CNF is satisfiable—the so-called "SAT' problem.
展开▼
