We are looking at propositional functions, any function that contains some element of boolean truth in the domain. Admittedly I'm a bit confused by this. Why do we use propositional logic? Formal logic is used to design safety critical systems. It helps reach bug free code. A safety property could be a threshold for temperature in a reactor. Used in chip design since intelligence disaster. Logic such as ITL has lead to better software design... It can control systems that are mutually exclusive. Lambda calculus semantic base for PL such as the shift to a functional paradigm. Type inference is built around formal logic. Getting a better understanding of the application of propositional logic and its relevance to ITL.
A proposition is an atomic entity true or false. Propositional variables represent specific propositions usually P and Q. meta variables such as f1 f2 f3... Can be assigned sets of true and false, consider f1 being a handle to (Q U P) where U is union is a very limited character set.
Logical operators combine variables for expressions. Starting to look a lot like axoims we used last year. BNF grammar can be used to describe propositional syntax.
f ::= true | P |! f | f1 AND f2.
Various transformation using de Morgans laws etc mean this is a suitable syntax for describing the entire syntax (nb ! Symbol denotes not on a limited charset and in upper case is a boolean and.)
Propositions can be satisfiable, valid or unsatisfied.
Valid means all possible inputs result in true. Satisfied means at least 1 permutations of variables results in true. Unsatisfied means no matter the input it cannot result in true.
No comments:
Post a Comment