# Questions tagged [automated-theorem-proving]

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

41 questions
Filter by
Sorted by
Tagged with
226 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 ...
160 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: ...
49 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 ...
284 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 ...
461 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: ...
395 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. ...
366 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)...
150 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 ...
154 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 ...
185 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 ...
225 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 ...
215 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 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 ...
267 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 ...
627 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-...
161 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 ...
132 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 ...
183 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 ...
222 views

935 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 ...
76 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 ...
547 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 ...
277 views

### Are there applications of experimental mathematics in TCS?

In recent years there have been major, diverse, sometimes surprising advances in experimental mathematics  for a variety of sophisticated uses such as developing/deriving exact formulas, theorem ...
797 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 ...
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 ...
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 ...
2k 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 ...
313 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, ...
723 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 ...
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 ...
407 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 ...
608 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 ...
841 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 ...