brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2024-11-12 12:00:35 -05:00
Code Issues Projects Releases Packages Wiki Activity

Added a definition to a post

Browse source
This commit is contained in:
Brandon Rozek 2021-12-15 14:07:16 -05:00
parent 48cba94803
commit ceedd3a003
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
content/blog/proofdef.md
View file

@ -9,9 +9,10 @@ math: true
When I look into a new field, sometimes I get confused by the whole new set of vocab terms I need to encounter. This post will serve to keep me straight with the terms involved in theorem proving. When I look into a new field, sometimes I get confused by the whole new set of vocab terms I need to encounter. This post will serve to keep me straight with the terms involved in theorem proving.
| Word | Definition | | Word | Definition |
| ------------ | ------------------------------------------------------------ | | ----------------- | ------------------------------------------------------------ |
| Modus Ponens | If $P$ implies $Q$ and $P$ is asserted to be true, then $Q$ must be true. | | Modus Ponens | If $P$ implies $Q$ and $P$ is asserted to be true, then $Q$ must be true. |
| Complete | If every formula having the property can be derived using the system. (i.e The system does not miss a result) | | Complete | If every formula having the property can be derived using the system. (i.e The system does not miss a result) |
| Negation-Complete | Either $\phi$ or $\neg \phi$ can be proved in the system. |
| Decidable | An effective method exists for deriving the correct answer in a finite time. | | Decidable | An effective method exists for deriving the correct answer in a finite time. |
| Sound | Every formula that can be proved in the system is logically valid with respect to the semantics of the system. (i.e The system does not produce a wrong result) | | Sound | Every formula that can be proved in the system is logically valid with respect to the semantics of the system. (i.e The system does not produce a wrong result) |