Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [automated-theorem-proving]

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

Filter by
Sorted by
Tagged with
0 votes
0 answers
14 views

Finding a common variable value among all SAT solutions

Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
csaltachin's user avatar
1 vote
1 answer
32 views

Topological/metric space formed by behaviors of distributed system: Safety and Liveness

In the book A Science of Concurrent Programs Leslie Lamport describes alternative way how to look at safety and liveness properties in distributed algorithms. A.5 Another Way to Look at Safety and ...
Andreo's user avatar
  • 113
0 votes
0 answers
15 views

how to model time and digital circuits in theorem prover

Most papers that I have seen on proving digital logic focus only on the combinational circuits (ie using boolean logic). But real life circuits also have flip-flops, ie a time element an a clock. How ...
R71's user avatar
  • 101
0 votes
1 answer
105 views

How to start with verifying a formal proof programmatically?

I heard the terms "theorem provers" and "proof assistants" tossed around before (which I assumed to be the same up until a couple seconds ago), and also of Coq, Idris, Agda, TLA+ (...
toraritte's user avatar
  • 105
8 votes
1 answer
2k views

What is the complexity of theorem proving?

I'm learning some computer science and mathematics by myself. I know that proving theorems in ZFC is undecidable in general, but, is there a formal way to express how complex it is? Is it as complex ...
Otakar Molnár López's user avatar
1 vote
1 answer
64 views

Automated theorem provers using models

I am wondering if they are automated theorem provers which can take as input known models of the theory, for example to help discard statements which are not correct. For example, if the statements ...
Julien Narboux's user avatar
1 vote
1 answer
93 views

Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?

I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ...
Vivek Joshy's user avatar
0 votes
1 answer
3k views

MergeSort's merge function loop invariant

I am reading a proof of correctness for the MergeSort Algorithm. This is the code for the MergeSort and the Merge function: The correctness of the MergeSort function is easy to prove since the two <...
mateleco's user avatar
  • 108
0 votes
2 answers
972 views

DFA and NFA Equivalence Proof

I'm taking a Theory of Computation class and we went over the proof to show that for any NFA there is an equivalent DFA, which I understand the proof fully in this case. But if it were in reverse, for ...
KJC_'s user avatar
  • 1
3 votes
1 answer
302 views

Building non-classical logics in Agda & Coq

Is it possible to construct different systems of logic in Coq or Agda? I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, ...
Kevin Flowers Jr's user avatar
3 votes
1 answer
98 views

Automated Query Equivalence Solver (MongoDB)

The query-equivalence problem is undecidable. However there are theorem provers that attempt to solve instances of undecidable problems. I am curious how I could go about using an automatic theorem ...
himself000's user avatar
2 votes
0 answers
79 views

Can all of math be automated?

Is this correct? Here's my reasoning. (Definition) Math is anything that can be proved from axioms. (Assumption) All (finite length) axiom sets can be enumerated. (Assumption) All (finite length ...
Jesus is Lord's user avatar
2 votes
1 answer
494 views

How to transform an Abstract Syntax Tree (AST) to an Abstract Binding Tree (ABT)? (for machine learning fo theorem proving)

I was reading the HOList paper that applies Graph Neural Networks (GNNs) to the HOL Light (HOList) data set and benchmark for ML for theorem proving. They describe their results etc but there is no ...
Charlie Parker's user avatar
1 vote
1 answer
53 views

Need help understanding Knuth's proof that: The set of all pure words is well-ordered by the relation >

In the paper linked below by Knuth and Bendix, theorem 1: The set of all pure words is well-ordered by the relation '$>$' has a proof that I can't seem to follow despite staring at it all day. I ...
frabrooks's user avatar
4 votes
0 answers
57 views

Do FOL theorem provers accept axiom schemata?

Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata? I looked in the Vampire "manual" briefly,...
MWB's user avatar
  • 505
1 vote
2 answers
210 views

Automated reasoning with real numbers

I have a large number of equivalences which look like: $(a \leq 0.54 \wedge b \geq 0.12) \vee (c \gt 0.98)$ $\Leftrightarrow$ $(x \leq 0.25) \vee (x \gt 0.91 \wedge y \geq 0.01)$ This is just an ...
Velvet Ghost's user avatar
2 votes
1 answer
166 views

What were the shortcomings of Robinson's resolution procedure?

Paulson et alii. From LCF to Isabelle/HOL say: Resolution for first-order logic, complete in principle but frequently disappointing in practice. I think complete means they can proof any true ...
user1868607's user avatar
  • 2,194
1 vote
3 answers
333 views

Prove simple theorems in Haskell in automated way

I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as: ...
Борат Сагдиев's user avatar
2 votes
3 answers
201 views

Halting problem vs. automated theorem proving?

In the Theory of Computation tutorial offered by Complexity Tree (I just began the 2nd video), it talks about how the Halting problem was developed to show that mathematics could not be automated. ...
cepheid's user avatar
  • 23
1 vote
1 answer
109 views

on coq: Why is the proof complete after proving only for one induction when we have more than one variable?

So I'm learning coq. And I came across the proof for associativity in addition forall (a b c : nat) Appearntly when we do ...
Archy Will He 何魏奇's user avatar
3 votes
1 answer
509 views

How to get an element from an existential proposition in Type theory proof assistant (Lean prover)

I am trying to implement set theory in type theory from scratch, just for self pedagogical purposes. Specifically, I'm using the Lean Prover, and defining the element-of relation from scratch using ...
user56834's user avatar
  • 3,892
2 votes
2 answers
239 views

How the kernel works in a LCF theorem prover

I heard that there is some mechanism in LCF-based theorem provers that only allows some functions to create values of type theorem. I believe these are based on abstract data types. Could someone ...
EvaMGG's user avatar
  • 167
39 votes
5 answers
6k views

Do theorem provers demonstrate their own correctness?

I am not very well-versed in the world of theorem proving, much less automated theorem proving, so please correct me if anything I say or assume in my question is wrong. Basically, my question is: are ...
J. Auon's user avatar
  • 503
1 vote
0 answers
31 views

Review of Formal Verification and How to Apply it to Greenfield Project [duplicate]

Last year I looked heavily into Formal Verification, such as automated theorem proving, model checking, type systems, symbolic evaluation, and many others. I probably spent a few weeks or maybe months ...
Lance's user avatar
  • 2,243
4 votes
0 answers
70 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 ...
Alex's user avatar
  • 263
2 votes
0 answers
38 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, ...
rwallace's user avatar
  • 386
1 vote
1 answer
54 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 ...
rwallace's user avatar
  • 386
1 vote
1 answer
38 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 ...
rwallace's user avatar
  • 386
7 votes
1 answer
459 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 ...
eins6180's user avatar
  • 171
2 votes
0 answers
70 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 ...
Cris P's user avatar
  • 121
1 vote
0 answers
83 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 ...
user56834's user avatar
  • 3,892
2 votes
0 answers
42 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 ...
user56834's user avatar
  • 3,892
2 votes
1 answer
59 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 ...
user1868607's user avatar
  • 2,194
2 votes
0 answers
75 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 ...
Joey Eremondi's user avatar
3 votes
1 answer
39 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 ...
Tyler Spaeth's user avatar
1 vote
0 answers
23 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:...
michalk93's user avatar
14 votes
1 answer
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-...
Math-fort's user avatar
  • 173
2 votes
1 answer
141 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: ...
K. Smith's user avatar
4 votes
0 answers
50 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 ...
Joey Eremondi's user avatar
5 votes
1 answer
134 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 ...
PKG's user avatar
  • 1,489
14 votes
1 answer
2k 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 ...
Walter Schulze's user avatar
5 votes
1 answer
84 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 ...
Dima Chubarov's user avatar
5 votes
1 answer
194 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 ...
user1868607's user avatar
  • 2,194
3 votes
0 answers
45 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 ...
user1868607's user avatar
  • 2,194
8 votes
1 answer
316 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 ...
user1868607's user avatar
  • 2,194
0 votes
1 answer
61 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 ...
Pushpa's user avatar
  • 933
1 vote
1 answer
117 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 ...
user2754673's user avatar
5 votes
1 answer
63 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, ...
MaiaVictor's user avatar
  • 4,137
8 votes
2 answers
275 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 ...
MaiaVictor's user avatar
  • 4,137
2 votes
0 answers
86 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 ...
user385223's user avatar