Automated theorem proving is the proving of mathematical theorems by a computer program.

learn more… | top users | synonyms

0
votes
1answer
56 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 ...
0
votes
0answers
101 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 ...
7
votes
1answer
123 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 ...
2
votes
0answers
136 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 ...
2
votes
0answers
46 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 ...
0
votes
2answers
161 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 ...
9
votes
1answer
129 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 ...
2
votes
0answers
284 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 ...
0
votes
1answer
154 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 ...
4
votes
0answers
99 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 ...
9
votes
2answers
444 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 ...
2
votes
0answers
65 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 ...
9
votes
3answers
463 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
219 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 ...
9
votes
1answer
571 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
109 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 ...
6
votes
2answers
640 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 ...
-5
votes
1answer
1k 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
269 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, ...
15
votes
4answers
548 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 ...
15
votes
2answers
958 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
248 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 ...
13
votes
6answers
559 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 ...
25
votes
1answer
698 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
297 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) ...
27
votes
2answers
1k 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 ...