Automated theorem proving is the proving of mathematical theorems by a computer program.
1
vote
0answers
61 views
loop invariants in proving program termination
consider two similar pieces of (pseudo)code:
A:
n = f(x)
for (i = 1 to n) do
begin
....
end
B:
x = 1
while (x != 0) do
begin
x = g(x)
....
end
in case A if ...
7
votes
3answers
384 views
Proofs found by computer
In 1996, a long-standing open problem was solved by a computer; namely, that Robbins algebra and Boolean algebra are the same. The proof was found by an automated theorem prover.
Moreover, the known ...
4
votes
0answers
173 views
Are there applications of experimental mathematics in TCS?
In recent years there have been major, diverse, sometimes surprising advances in experimental mathematics [1] for a variety of sophisticated uses such as developing/deriving exact formulas, theorem ...
6
votes
1answer
255 views
Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?
This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory.
The post makes the claim of a future 'unification' between the the describing language of math, and the operation ...
2
votes
1answer
87 views
How to auto-derivate sequential iterative programs from a mathematical specification?
I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory.
First, write down the formal specification as a Hoare triple and figure ...
3
votes
1answer
273 views
Automated theorem proving via unsupervised approaches
This question Where and how did computers help prove a theorem? considers some automated theorem proving successes.
However they seem to be mostly supervised approaches, such as with the 4 color graph ...
-4
votes
1answer
565 views
Proof that DFA that accepts string has NFA that accepts reversal of string
I have seen descriptions for an algorithm that can take a regular deterministic finite automata and create a non-deterministic finite automata that is guaranteed to generate the reverse of string ...
3
votes
3answers
234 views
Automatic proofs or model checking in an extremely simplified functional language
Imagine a stripped down functional programming language, that has the following properties
The only value type is an integer
There are no side effects
Functions are defined as a single expression, ...
10
votes
3answers
325 views
Automated theorem proving in linear logic
Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction? Where can I read more about automatic theorem proving in these ...
13
votes
2answers
640 views
Why is it so difficult for a computer to prove something?
This may be considered a stupid question. I am not a computer science major (and I'm not a mathematics major yet, either), so please excuse me if you think that the following questions display some ...
6
votes
1answer
172 views
reference for lexicographic path ordering
Can you recommend a good reference for reading about lexicographic/recursive path orderings?
I'm currently reading about lpo's in Chapter 2 of the Handbook of Automated Reasoning, 'Resolution Theorem ...
11
votes
6answers
438 views
What are practically computable properties of Labelled Transition Systems?
I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would ...
21
votes
1answer
580 views
Is there a reasonable automated proof system for TCS theorems?
Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I ...
10
votes
2answers
233 views
Are there semi-decision procedures for this theory?
I have the following typed theory
|- 1_X : X -> X
f : A -> B, g : B -> C |- compose(g,f) : A -> C
F, f : A -> B |- apply(F,f) : F(A) -> F(B)
...
22
votes
2answers
918 views
If P=NP, could we obtain proofs of Goldbach's Conjecture etc.?
This is a naive question, out of my expertise; apologies in advance.
Goldbach's Conjecture and many other unsolved questions in mathematics can be written
as short formulas in predicate calculus.
For ...
