Questions tagged [automated-theorem-proving]
Automated theorem proving is the proving of mathematical theorems by a computer program.
49
questions
6
votes
1
answer
221
views
What's the state of research on automated theorem proving?
I'm interested in writing my undergraduate thesis on automated theorem proving, and I've been looking for some material to document myself on the topic.
I was introduced to automated and assisted ...
- 163
12
votes
0
answers
229
views
Have any well-known results been refuted by a theorem prover?
Have any well-known results in mathematics or computer science been shown to be false through the use of a theorem prover or proof assistant? I am not interested in cases where the proof of a true ...
- 221
4
votes
0
answers
183
views
What logic do refinement types correspond to?
I'm interested in applicability of refinement types to theorem-proving hence the questions about their logical expressiveness. Let's say, we have a type system which corresponds to some logic ...
- 41
0
votes
1
answer
237
views
Automatic theorem prover for first-order logic versus model checker
What's the formal difference between a model checker, and an automated theorem prover for first-order logic, i.e. something like Meson/Metis/Sledgehammer/Vampire/E? Link to a clear discussion of the ...
- 841
4
votes
0
answers
129
views
A reasonable proof strategy for formally verifying Ukkonen's algorithm?
What's a reasonable proof strategy to formally verify Ukkonen's algorithm in, say, Coq? The ingredients as far as I can tell would be:
some form of separation logic to be able to reason about the ...
- 585
1
vote
0
answers
80
views
Journals or conferences to submit formally verified libraries?
This is a soft question aimed at understanding whether there is any value to publishing formally verified libraries. I have formally verified (in Coq) implementations of:
synthetic differential ...
- 585
2
votes
1
answer
332
views
Extensional type theory and function extensionality
Is the principle of function extensionality
$ (\forall x. f(x) = g(x)) \implies f = g$, derivable from ETT?
Most notably is this derivable in Agda with axiom K?
- 841
5
votes
0
answers
177
views
On the interpretation of coinduction in type theory
The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal ...
- 889
9
votes
1
answer
384
views
Turing Machines as Coalgebras
I'm looking to write a survey on the method of representing the dynamics of state-based computation within the framework of coalgebras. So far I've managed to find papers on coalgebra representations ...
- 163
6
votes
1
answer
258
views
General Induction Principle
Let us suppose that we want to provide for each inductive type an axiom describing the associated elimination/induction principle. For example, given a definition for the naturals:
...
- 175
4
votes
0
answers
56
views
Formalization of Interval Newton methods in a proof assistant or theorem prover
I am undertaking the task of formalizing Interval Newton Methods in Isabelle. To the best of my knowledge this hasn't been formalized in other proof assistants or theorem provers. However, I want to ...
- 889
4
votes
1
answer
376
views
If a root||nonce Proof-of-Work certificate is prime, can it be used in any other interesting proofs?
Because Bitcoin and many other cryptocurrency mining certificates are "rare" in that their respective hash is less than a very small number, can we leverage their rarity in probabilistic proofs of ...
- 852
4
votes
0
answers
512
views
Is it possible to derive induction by extending CoC with recursion?
Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms:
...
- 3,035
11
votes
2
answers
449
views
State of the Art for the Monadic Class?
Monadic First Order Logic, also known as the Monadic Class of the Decision Problem, is where all predicates take one argument. It was shown to be decidable by Ackermann, and is NEXPTIME-complete.
...
- 2,764
2
votes
2
answers
405
views
Automated proving that a program doesn't halt
If you are a computer and you are given a program $P$ (with no input parameter) that doesn't halt, how would you try proving it doesn't halt ? (here proving means convincing ourselves that it is true)...
- 145
0
votes
1
answer
189
views
Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem?
Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem？ In other words, could the Tarski–Seidenberg theorem subsume Buchberger's algorithm and Wu's ...
- 1,050
4
votes
1
answer
230
views
resolution based theorem prover for temporal logic
I am looking at implementing a a resolution-based theorem prover for propositional linear temporal logic (PLTL) (as opposed to a model checker). The ones out there (by Fisher et. al. and others) are ...
- 141
8
votes
0
answers
213
views
Is there a known automatic proof of the independence of the continuum hypothesis?
In 2002, L.C. Paulson gave a mechanized proof of the consistency of the axiom of choice by formalizing $V=L$ and its consistency. We could ask whether there is a formalized proof of the independence ...
- 181
5
votes
1
answer
241
views
Mechanization of Mathematics
Its been a while since I took my theory course, but I recall that Hilberts Decision problem was shown to be false.
By the completeness theorem of first-order logic, a statement is universally valid ...
- 75
15
votes
1
answer
264
views
How to determine whether a proof requires "higher-order reasoning techniques"?
The question:
Suppose I have a specification of a problem consisting of axioms and a goal (i.e. the associated proof problem is whether the goal is satisfiable given all the axioms). Let us also ...
- 159
8
votes
1
answer
213
views
What is the significance of nominal techniques?
What is the significance of nominal techniques, as far as their application to the formal theory of bound variables is concerned?
I have been reading M. J. Gabbay's expository work on the topic that ...
15
votes
1
answer
523
views
Logical Reations for an Impredicative System in a Predicative MetaTheory
Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
- 1,518
9
votes
1
answer
669
views
Why is Proof Checker required in Proof Carrying Code
In the classical PLDI'98 paper by Necula, "The design and implementation of a certifying compiler", the high-level verifier uses:
VCGen to generate verification conditions (safety predicates)
First-...
- 193
0
votes
1
answer
189
views
Is there an algorithm to generate proof in Coq? [closed]
I try to imagine using Coq to implement large and complicated software with specifications and proof. However, the manual work of writing proof is daunting. As a Coq newbie, to specify an insertion ...
- 159
1
vote
0
answers
150
views
Do problems have to be statable in $\Pi_1$ to use Levin's universal search to find short proofs if P=NP
In If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? it talks about the hypothetical world where P=NP and using the proof of it to prove a problem/theorem assuming that it has a short ...
- 21
7
votes
1
answer
215
views
Formalized priority argument
A priority argument, an important proof technique in recursion theory, was introduced by Friedberg and Muchnik, to solve Post's Problem, i.e., the existence of two r.e. sets that do not Turing reduce ...
- 885
4
votes
1
answer
249
views
Looking for reference on NP-Completeness of proofs of length n
Given a deductive system $\Lambda$, and some well-formed-formula S, one can ask the question "Is there a proof S in $\Lambda$ of length n?" If n is presented in base-1 and if all the axioms of $\...
- 415
3
votes
1
answer
150
views
Can we verify satisfiability of first order statements via saturation in sub-exponential time?
In first order logic, we can prove satisfiability several ways: Finite model generation, truthful monadic abstractions, and also saturation. With finite model generation techniques, we can verify the ...
- 318
0
votes
2
answers
233
views
Logic with Linear Programming
Can first-order logic be modeled/simulated as linear programming or integer programming?
What about other forms of logic (say second order)?
Update: am actually not a theory person, but more on the ...
- 749
9
votes
1
answer
567
views
First order satisfiability that doesn't have finite models
We know from Church's theorem that determining first order satisfiability is undecidable in general, but there are several techniques we can use to determine first order satisfiability. The most ...
- 318
2
votes
0
answers
388
views
Theorem prover fails to find simple set theory proof?
I am trying to use an automated theorem prover (SNARK) to prove a theorem in first-order logic.
Tarski claims in his "a work on mereology" that
the goal is provable from assertions 1-3 but he does ...
- 279
2
votes
2
answers
821
views
Which formalism is best suited for automated theorem proving in set theory?
Abbreviations - FOL is first-order logic; NBG is Von Neumann–Bernays–Gödel set theory; SEP is Stanford Encyclopedia of Philosophy; HOL is higher-order logic; ATP is automated theorem proving.
Context ...
- 279
5
votes
0
answers
120
views
extracting/ exploiting similarity of SAT instances by solver
suppose that two SAT formulas on different variables $F_1, F_2$ are given on the input that are known to be true and the problem is to build an algorithm that finds a solution to each. the formulas ...
- 10.9k
11
votes
2
answers
1k
views
What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?
I am in possession of a book, which, inspired by Russell's Principia Mathematica (PM) and logical positivism, attempts to formalize a specific domain by determining axioms and deducing theorems from ...
- 279
2
votes
0
answers
79
views
Regaining decidability by adding axioms that model real world situation
It is known that first order logic is too general to be decidable. Adding axioms with special meaning (e.g. expressing notions such as necessity/obligation, provability, etc.) leads us to modal logics ...
- 409
11
votes
3
answers
612
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,011
5
votes
0
answers
299
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 ...
- 10.9k
10
votes
1
answer
884
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,541
2
votes
1
answer
125
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 ...
- 23
8
votes
2
answers
1k
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 ...
- 10.9k
-5
votes
1
answer
3k
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 ...
- 7
3
votes
3
answers
331
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, ...
- 185
18
votes
4
answers
841
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 ...
- 4,001
18
votes
2
answers
2k
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 ...
- 637
6
votes
1
answer
537
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 ...
- 189
14
votes
6
answers
671
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 ...
- 241
29
votes
1
answer
919
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 ...
user1338
10
votes
2
answers
477
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)
...
- 221
36
votes
2
answers
2k
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 ...
- 3,703