Questions tagged [automated-theorem-proving]

Machine-checked, machine-generated or machine-verified proofs

Filter by
Sorted by
Tagged with
44
votes
6answers
8k views

Learning Automated Theorem Proving

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Note that these topics are not easily digested ...
20
votes
1answer
1k views

Types of Automated Theorem Provers

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Which are the relevant automated theorem provers? I ...
17
votes
3answers
3k views

Why is unification so important to inference engines?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...
16
votes
2answers
365 views

Why do some inference engines need human assistance while others don't?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Why is it that automated theorem provers, i.e. ACL2,...
13
votes
1answer
1k views

What kind of math problems can be solved by automated theorem provers?

Can I prove following statements with using available automated theorem provers? $(a+b)^2=a^2+b^2+2ab$. If $ 11 \mid 2a-3b$, then $ 11 \mid 7a-5b $. If $ ax^2+bx+c=0$, then $x=\frac{-b\pm\sqrt{b^2-...
13
votes
1answer
622 views

Monadic Second Order Logic for Dummies

I am programmer with a grip on automata, but not on logic. I read in papers that the two are very tightly related. Deterministic Finite Automata (DFA), Tree Automata and Visibly Pushdown Automata are ...
11
votes
1answer
223 views

How did 'Isabelle' (the theorem prover) get its name?

The title says it all, but I'm curious because it isn't obvious how a theorem prover came to be named 'Isabelle'. Was it named for a person? I couldn't find out by some Google searches.
10
votes
2answers
2k views

Theorem Proofs in Coq

Background I am learning assistance, Coq, on my own. So far, I have completed reading Yves Bertot's Coq in a Hurry. Now, my goal is to prove some basic results concerning the natural numbers, ...
10
votes
1answer
475 views

Distinct variables for different clauses

In resolution theorem proving, it is normally assumed variables in different clauses are distinct. This is not something that happens automatically; it requires significant extra code and computation ...
7
votes
1answer
217 views

What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?

I'm reading through a commentary on Milner's "The use of machines to assist in rigorous proof" by Mike Gordon. In this paper, he explains how LCF was born from the ideas of denotational semantics by ...
7
votes
2answers
158 views

Why Church-encoded types aren't sufficient to express inductive proofs?

I've heard some claims that the calculus of constructions without inductive types isn't powerful enough to express proofs by induction. Is that correct? If so, why isn't the Church-encoding sufficient ...
7
votes
1answer
257 views

Redundancy elimination in the superposition calculus

When proving theorems with the superposition calculus, we deal with three kinds of rules: Generating rules: from pair of clauses A and B, generate new clause C while keeping the original pair, e.g. ...
6
votes
1answer
685 views

Why is automated theorem proving impossible?

As far I know, in general case there is no Turing machine which could get any theorem on its input and produce its proof on its output. Why is it so?
6
votes
1answer
203 views

Framework or tools to generate theorem prover/solver/reasoner for new logic

I have new logic which has syntax and semantics in usual natural languages and I have to create theorem prover/solver/reasoner for this logic. Is there framework or tool set that can generate such ...
5
votes
1answer
92 views

Why do presenttations of proof systems in logic and automated reasoning not include the algorithm that finds proofs?

Is is that a common way to present a proof system in the field of Logic and Automated Reasoning is to present a system of inference rules, without having to formally describe a particular algorithm or ...
5
votes
1answer
56 views

Is it possible to build short proofs of arbitrary folds over a huge list?

With the use of Merkle Trees, you can prove the presence of an element of a very big list, with an amount of information close to just logarithm of the size of the whole tree. Merkle proofs, thus, ...
5
votes
2answers
684 views

Automated geometric theorem-proving using synthetic methods

This question is about geometric theorem proving and is inspired by this Math.SE post. Currently, Euclidean-geometric theorem provers, as referred to in the post, use coordinate geometry to convert ...
5
votes
1answer
68 views

Why do TPTP Performance plots look like this?

CASC is the premier Automated Theorem Prover competition performed annually at the Conference on Automated Deduction (CADE). The 2017 event has finished on the 9th of August this year. During this ...
5
votes
1answer
152 views

Procedure to automatically solve field theorems in a SMT solver

I'm working with the Welder proof assistant. Basically, this system uses basic inference rules to modify the goal one wants to proof. At a latter step, the modified goals are passed to a SMT solver to ...
5
votes
1answer
969 views

Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
4
votes
1answer
418 views

What happens to uninterpreted predicates in Ackermann's reduction?

I know the procedure to apply the Ackermann's reduction to a formula that doesn't involve uninterpreted predicates. But, how do we treat the uninterpreted boolean predicates? Nearly all the examples I ...
4
votes
1answer
1k views

What is the difference between “definition” and “inductive” in Coq?

In Coq, you can use two different kinds of keywords to do definitions--Inductive and Definition. I do not understand the difference between an inductive and a definition, or when it is appropriate to ...
4
votes
1answer
122 views

Roadmap to formal verification

I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also ...
4
votes
1answer
266 views

Proof Carrying LLVM?

I am intrigued by and understand the very basics of Proof Carrying Code (PCC) and I recognize that LLVM is a machine-independent intermediate language. LLVM is the intermediate form of many languages,...
4
votes
0answers
40 views

Modern presentation of Ackermann's “Solvable Cases?”

Ackermann's book "Solvable Cases of the Decision Problem" discusses decidable instances of first order logic, particularly monadic logic, and so called "equality formulas". However, the book is from ...
3
votes
2answers
2k views

Equivalence of NFA and DFA - proof by construction

I was looking at the construction proof showing the equivalence of NFA and DFA from Sipser's text. It started by taking number of states of DFA as $\mathcal{P}(Q)$, where $\mathcal{P}(Q)$ is the set ...
3
votes
1answer
135 views

How can I check constraints on my state machine behaviour?

My background is fairly practical rather than theoretical, so this question may be a bit basic. I have a state machine with events, and events may optionally trigger action functions to be called as ...
3
votes
1answer
62 views

Theorem Prover for complexity theoretic reductions

Can complexity theoretic reductions that lead to proofs of say NP completeness be formalized using an existing theorem prover such as Coq? If so, can you provide an outline of how to formalize a ...
3
votes
1answer
402 views

What is the difference between superposition and paramodulation?

I am currently writing a paper about automated theorem proving in first-order logic. Equality is not uncommon for mathematical problems and almost every theorem prover like VAMPIRE or SPASS has a ...
3
votes
0answers
35 views

Is there a correspondence of steps between DPLL and sequent-calculus?

Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid? And given ...
3
votes
0answers
40 views

Sorts and constructors for modelling classes in a theorem prover

I have been working in the Welder theorem prover for some time now. But I'm confused in the way they handle data-types. I'm not familiar with the terminology of sorts and constructors. Here is how one ...
2
votes
1answer
299 views

Automated theorem proving with SAT

If you had a polynomial time algorithm for determining boolean satisfiability how would you prove/disprove a conjecture like the Reimann-Zeta hypothesis (or the Pythagorean theorem for that matter) ...
2
votes
1answer
25 views

Has the concept of using a hand checked simple theorem prover to validate more complex theorem provers been explored before?

More specifically, has anyone used a chain of theorem provers to validate a highly evolved theorem prover, starting with a very simple hand checked prover such that each new theorem prover is used to ...
2
votes
1answer
60 views

How to define function type in AGDA

The "function" type $\rightarrow$ is predefined in Agda. But how would one define it if it was not predefined? Specifically I am talking about $\rightarrow$ in: ...
2
votes
1answer
32 views

Derivation of implicational propositional axioms

Is there a way to subtract and add properties of axioms to generate new axioms? For example: {L} = {P S K} // natural deduction {P S K} = {P H K I} // natural deduction {S K} = {?} // constructive ...
2
votes
0answers
30 views

Superposition calculus: greater vs greater-or-equal

Bachmair and Ganzinger 1991, 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', specifies the criterion for using an equation as, by some appropriate ordering, ...
2
votes
0answers
45 views

Unification algorithm that directly finds multiple substitutions?

Systems of formal logic generally have inference rules that require certain expressions to be syntactically the same in multiple steps. Typically two steps are involved, as for modus ponens, where ...
2
votes
0answers
19 views

Why aren’t (type theory based) automated theorem provers efficient?

Note: my main experience with theorem provers is with Type theory based proof-assistant, rather than an actual automated theorem prover. It is obvious why naive automated theorem proving is ...
2
votes
0answers
52 views

Are there any interesting terms in pure LF or $\lambda\Pi$?

In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$. I know that LF and the dependently typed ...
2
votes
0answers
70 views

How to self-learn automated theorem proving? [duplicate]

Year 12 high school student here, but my ambition is set on Automated Theorem Proving. I wish to apply it to, of course, mathematics and computer science, and maybe if possible other applied subjects ...
1
vote
1answer
31 views

Superposition calculus: Elimination of redundant atoms

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', section 5.2, 'Simplification and Deletion Techniques', page 17, 'Elimination of redundant ...
1
vote
1answer
44 views

Finding libraries of formalized mathematics

I want to formalize Interval Newton Methods in Isabelle. As a research, I have the curiosity of whether there is anything done in the field. For that, I need to know what mathematical contents have ...
1
vote
1answer
25 views

Bachmair and Ganzinger, ordering of equations

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical ...
1
vote
1answer
50 views

How to reduce constrained proofs to 0-1 IP

Consider the following problem: Can $X$ be proven in fewer than $Y$ steps, from axioms $Z$, with finitely many transition rules $\tau$? This lies in $NP$, since if I supply a proof $M$, and ...
1
vote
0answers
60 views

Type theory based automated theorem prover?

I know that there exist type theory based proof-checker, and I know that there are logic/sequent-calculus based automated theorem provers. But I haven’t heard of a type-theory based automated theorem ...
1
vote
0answers
16 views

Differentiate arguments in SPASS prover formula

I have a formula in FOL: $\forall x \exists y: B(x) \implies C(y)$ and in SPASS: forall([X], exists[Y], implies(B(X),C(Y))) I want to check the formula: $\exists x:...
1
vote
1answer
90 views

Formal specification; Logical formula

* Initial Question * I'm trying to write a logical formula consists of three Boolean variable C1, C2, C3. My program takes graph as input and checks properties about them. C1 represents presence of ...
1
vote
0answers
73 views

sets of axioms for LADR automated theorem provers

I am pretty new to ATP, but I'm really enjoying playing around with prover9. I have found a nice set of axioms for basic information-theoretic proofs here, I was wondering if there are some ...
0
votes
1answer
51 views

Verification condition in case of array theory

As far as i can understand the problem of checking safety property, can be reduce to solving for inductive invariants in VC's and there is following parts to it: Generate VC's from the program. Solve ...