Questions tagged [automated-theorem-proving]

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

Filter by
Sorted by
Tagged with
3 votes
0 answers
77 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 ...
user avatar
12 votes
0 answers
226 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 ...
user avatar
4 votes
0 answers
165 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 ...
user avatar
  • 41
0 votes
1 answer
179 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 ...
user avatar
  • 723
4 votes
0 answers
117 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 ...
user avatar
1 vote
0 answers
79 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 ...
user avatar
1 vote
1 answer
261 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?
user avatar
  • 723
5 votes
0 answers
167 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 ...
user avatar
9 votes
1 answer
363 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 ...
user avatar
  • 163
6 votes
1 answer
236 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: ...
user avatar
  • 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 ...
user avatar
4 votes
1 answer
363 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 ...
user avatar
  • 822
4 votes
0 answers
505 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: ...
user avatar
  • 3,045
11 votes
2 answers
442 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. ...
user avatar
2 votes
2 answers
392 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)...
user avatar
0 votes
1 answer
181 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 ...
user avatar
4 votes
1 answer
222 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 ...
user avatar
  • 141
8 votes
0 answers
209 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 ...
user avatar
5 votes
1 answer
238 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 ...
user avatar
15 votes
1 answer
258 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 ...
user avatar
8 votes
1 answer
200 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 ...
user avatar
15 votes
1 answer
479 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 ...
user avatar
  • 1,412
9 votes
1 answer
664 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-...
user avatar
  • 193
0 votes
1 answer
184 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 ...
user avatar
  • 159
1 vote
0 answers
143 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 ...
user avatar
  • 21
7 votes
1 answer
207 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 ...
user avatar
  • 875
4 votes
1 answer
244 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 $\...
user avatar
3 votes
1 answer
148 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 ...
user avatar
  • 318
0 votes
2 answers
231 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 ...
user avatar
  • 739
9 votes
1 answer
452 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 ...
user avatar
  • 318
2 votes
0 answers
386 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 ...
user avatar
  • 279
2 votes
2 answers
783 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 ...
user avatar
  • 279
5 votes
0 answers
119 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 ...
user avatar
  • 10.8k
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 ...
user avatar
  • 279
2 votes
0 answers
78 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 ...
user avatar
  • 409
11 votes
3 answers
599 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 ...
user avatar
5 votes
0 answers
292 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 ...
user avatar
  • 10.8k
10 votes
1 answer
877 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 ...
user avatar
  • 2,501
2 votes
1 answer
122 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 ...
user avatar
  • 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 ...
user avatar
  • 10.8k
-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 ...
user avatar
  • 7
3 votes
3 answers
325 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, ...
user avatar
  • 185
18 votes
4 answers
825 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 ...
user avatar
  • 3,993
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 ...
user avatar
6 votes
1 answer
510 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 ...
user avatar
14 votes
6 answers
660 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 ...
user avatar
29 votes
1 answer
905 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 ...
user avatar
  • 5,070
10 votes
2 answers
468 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) ...
user avatar
  • 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 ...
user avatar