2024-03-01
The terminology surrounding logical reasoning in computer science is rather confusing, with a lot of overlap between different terms. And, to be honest, I’m not really even sure what to call the field as a whole.
Below is my understanding of the terms I’ve come across.
Disclaimer: I’m a novice trying to learn, not an expert, and these definitions come from me, not from a dictionary.
https://en.wikipedia.org/wiki/Formal_methods
This term is the most general and refers to a wide range of software/hardware specification/analysis techniques. The “formal” part means “mathematically rigorous” as well as “we didn’t just write some test cases and eyeball the code”.
https://en.wikipedia.org/wiki/Formal_verification
This term refers to applying formal methods to prove that some software or hardware is “correct” (satisfies a specification).
This is one of the “formal methods”. Titling a paper “Formally verifying such-and-such-program using theorem proving” would be correct usage.
It refers to proofs in mathematics, where a statement (a “theorem”) can be proven “true” by deducing it from other statements already considered “true”. A formal language is used to express the true-or-false statements and various “deduction rules” are applied to the statements to generate new statements. This process of checking that a proof was done correctly is entirely mechanical and does not require any human intuition.
The problem with this term is if you use it in a conversation with a mathematician they’ll look at you funny. Proving theorems is what mathematics is all about; it’s typically done informally with paper and pencil. From their perspective, it would be no more imprecise to refer to the process as “computer-running” instead of “theorem-proving”.
https://en.wikipedia.org/wiki/Automated_theorem_proving
This term is more specific than just “theorem proving” alone. It implies that the process of writing the proof has been automated in some way.
To some extent, a mathematical statement can be given to an automated theorem prover and a “true” or “false” value will be returned along with a list of deductions that were made to get to that value. It’s not possible to make an automated theorem prover that can correctly prove every expressible statement (or even most expressible statements) true or false, but there do exist ones that can prove many theorems with no help and many more theorems with some human guidance.
This term doesn’t sound generic like “theorem proving” alone, but it excludes non-automatic mechanical theorem proving tools, which are still very useful.
https://en.wikipedia.org/wiki/Proof_assistant
A proof assistant is a tool used for mechanical theorem proving. It can be automatic or manual. It might refer to the language in which statements are written, the proof checker, the automated proof generator, or all of the above.
https://en.wikipedia.org/wiki/Automated_reasoning
This term might refer to automated theorem proving or, more generally, any automated formal methods. Amazon Science seems to be using this definition (https://www.amazon.science/blog/a-gentle-introduction-to-automated-reasoning).
The term “reasoning” is also used in computer science for things beyond mathematical logic, like commonsense reasoning (https://en.wikipedia.org/wiki/Commonsense_reasoning), which makes the term slightly confusing (in my opinion).
https://en.wikipedia.org/wiki/Computational_logic
This term was originally proposed in the 1970s as a more accurate alternative for the term “theorem proving”. It seems to mean both “reasoning about computation using mathematical logic” as well as “mechanically implementing mathematical logic using computers”.
I personally think this term is the most precise, covering all of the desired topics without sounding too generic. Unfortunately I don’t see it used as much as “theorem proving”.
https://en.wikipedia.org/wiki/Logic_programming
Logic programming is a programming language paradigm; Prolog is the most prominent example. It’s based on a restricted form of mathematical logic that is possible to evaluate as a programming language.
I have done very little Prolog programming, but here is my understanding of the difference between Prolog and theorem proving: in Prolog the goal is to “fill in the blanks” of a desired logical statement, while in theorem proving the goal is to rewrite a statement into “true” or “false”. Both paradigms have a notion of “substituting equals for equals”, but in Prolog this substitution only happens in one direction for any given rule, while in theorem proving it can happen in both directions.
That being said, in Prolog you can deliberately include reversed versions of any rule, allowing for substitutions to occur in either direction, but this causes the prolog interpreter to loop infinitely (alternating between applying each rule).