This is an abridged account of Theorem Proving in Lean capturing only the SSPs, or super salient points.
Here are some three starting definitions essential for understanding this topic:
Formal verification - using logical and computational methods to establish claims that are expressed in precise mathematical terms. Example claims - mathematical theorem /hypothesis, claims that pieces of hardware or software, network protocols, security protocols - do what they say they actually do. The process is "describe your system in mathematical terms" ,then use "theorem proving" to establish truth.
Automated theorem proving - focused on "finding". The "ATP" toolkit includes: resolution theorem provers, tableau theorem provers, fast satisfiability solvers to provide means of establishing validity of formulas in propositional and first-order logic. Computer algebra systems may be used in concert to carry out mathematical computations.
Automated reasoning - differs; not as "cast iron" as theorem proving. Automated reasoning is a superset of automated theorem proving, which includes imprecise techniques such as heuristic search and fuzzy logic.
No comments:
Post a Comment