Questions tagged [automated-theorem-proving]
Machine-checked, machine-generated or machine-verified proofs
73 questions
1 vote
1 answer
87 views
Software that finds/proves runtime complexity of given code?
Is there software that can prove the runtime complexity of given code?
- 224
2 votes
1 answer
121 views
Z3 Exploration into Euler's Sum of Powers Conjecture Counterexample
I am trying to use z3 to come up with Ladner and Parkin's counterexample of Euler's Sum of Power's Conjecture which is a generalization of Fermat's Last Theorem. Euler's Sum of Power's Conjecture : ...
- 103
1 vote
1 answer
61 views
Topological/metric space formed by behaviors of distributed system: Safety and Liveness
In the book A Science of Concurrent Programs Leslie Lamport describes alternative way how to look at safety and liveness properties in distributed algorithms. A.5 Another Way to Look at Safety and ...
- 113
0 votes
1 answer
222 views
How to start with verifying a formal proof programmatically?
I heard the terms "theorem provers" and "proof assistants" tossed around before (which I assumed to be the same up until a couple seconds ago), and also of Coq, Idris, Agda, TLA+ (...
- 105
8 votes
1 answer
2k views
What is the complexity of theorem proving?
I'm learning some computer science and mathematics by myself. I know that proving theorems in ZFC is undecidable in general, but, is there a formal way to express how complex it is? Is it as complex ...
1 vote
1 answer
119 views
Automated theorem provers using models
I am wondering if they are automated theorem provers which can take as input known models of the theory, for example to help discard statements which are not correct. For example, if the statements ...
- 113
2 votes
2 answers
223 views
Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?
I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ...
- 121
0 votes
1 answer
5k views
MergeSort's merge function loop invariant
I am reading a proof of correctness for the MergeSort Algorithm. This is the code for the MergeSort and the Merge function: The correctness of the MergeSort function is easy to prove since the two <...
- 108
0 votes
2 answers
2k views
DFA and NFA Equivalence Proof
I'm taking a Theory of Computation class and we went over the proof to show that for any NFA there is an equivalent DFA, which I understand the proof fully in this case. But if it were in reverse, for ...
- 1
3 votes
1 answer
474 views
Building non-classical logics in Agda & Coq
Is it possible to construct different systems of logic in Coq or Agda? I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, ...
- 133
3 votes
1 answer
151 views
Automated Query Equivalence Solver (MongoDB)
The query-equivalence problem is undecidable. However there are theorem provers that attempt to solve instances of undecidable problems. I am curious how I could go about using an automatic theorem ...
- 31
2 votes
1 answer
150 views
Can all of math be automated?
Is this correct? Here's my reasoning. (Definition) Math is anything that can be proved from axioms. (Assumption) All (finite length) axiom sets can be enumerated. (Assumption) All (finite length ...
- 421
3 votes
1 answer
644 views
How to transform an Abstract Syntax Tree (AST) to an Abstract Binding Tree (ABT)? (for machine learning fo theorem proving)
I was reading the HOList paper that applies Graph Neural Networks (GNNs) to the HOL Light (HOList) data set and benchmark for ML for theorem proving. They describe their results etc but there is no ...
- 3,124
1 vote
1 answer
91 views
Need help understanding Knuth's proof that: The set of all pure words is well-ordered by the relation >
In the paper linked below by Knuth and Bendix, theorem 1: The set of all pure words is well-ordered by the relation '$>$' has a proof that I can't seem to follow despite staring at it all day. I ...
- 13
4 votes
0 answers
86 views
Do FOL theorem provers accept axiom schemata?
Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata? I looked in the Vampire "manual" briefly,...
- 515