# 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
147 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 ...
138 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 ...
691 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 ...
95 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 ...
171 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?
72 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 ...
149 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 ...
229 views

799 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 ...
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 ...
649 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 ...
588 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 ...
285 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 ...
856 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 ...
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 ...
321 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, ...
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 ...
883 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 ...
485 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 ...