# Questions tagged [automated-theorem-proving]

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

47 questions
Filter by
Sorted by
Tagged with
15 views

### Universal Generalisation Inference rule over array Proprties

I have a question about the soundness of the Universal Generalization Rule Over array Properties in proof i am working on To give some hints about the problem: suppose that $f(x)$ and $g(x)$ represent ...
114 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 ...
83 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 ...
53 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 ...
118 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?
128 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 ...
262 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 ...
183 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: ...
53 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 ...
298 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 ...
469 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: ...
417 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. ...
374 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)...
154 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 ...
190 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 ...
189 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 ...
239 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 ...
167 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 ...
312 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 ...
653 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-...
167 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 ...
134 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 ...
188 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 ...
226 views

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 ...
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 ...
575 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 ...
283 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 ...
833 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 ...
314 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, ...
766 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 ...
459 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 ...
632 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 ...
864 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 ...