Questions tagged [proof-assistants]

Applications that allow to create formal proofs. They assist the user by finding partial and checking complete proofs. General questions about proof assistants can also be asked on the Proof Assistants Stack Exchange site.

93 questions
Filter by
Sorted by
Tagged with
13 views

Transform OTM for Problem π to DTM ∈ DSPACE(n)

Given an Oracle Turing machine ($OTM$) that solves Problem π in max. 2n space, so $O(n)$ space and $O(n^2)$ time. Is there a DTM that can solve $π$ in $O(n)$ space if time doesn't matter? (The length ...
959 views

Curry-Howard isomorphism and non-constructive logic

My understanding of the Curry–Howard correspondence is that it shows an isomorphism between constructive logic (also called intuitionistic logic) and computer programs in appropriate typed languages. ...
• 231
102 views

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+ (...
• 105
53 views

Defining 2 inductive propositions relying on each other in Coq

I'm pretty beginner in Coq. I want to formalize negative and positive occurrence of an atom in a proposition inside coq the definition is as down below: I want to define this property as an Inductive ...
22 views

How do you prove a presence of GAN generated samples being exactly (or almost exactly) identical to real observations?

Suppose that $X\in\mathcal{X}$ is data in abstract space and $Z\in\mathcal{Z}$ is random noise vectors in latent space over a defined prior $P(Z)$ (e.g., Gaussian). Then, let $G$ and $D$ denote ...
899 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 ...
• 1
1 vote
151 views

Proving transitivity in an intuitionistic type theory without the K rule

In Agda, if I disable axiom $\mathbb{K}$ I'm not able to prove $$\forall\{A : \textbf{Set}\}\{a\ b : A\}\{p\ q : a \equiv b\} \to p \equiv q,$$ which I guess is normal since the system does not ...
284 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, ...
170 views

Difference between $\Rightarrow$, $\Longrightarrow$ and $\rightarrow$ in Isabelle/HOL?

I haven't been able to find a good explanation of how these are different and relate to each other. I know that $\to$ is part of HOL and $\Rightarrow$ and $\Longrightarrow$ part of Isabelle, but it ...
• 3,752
92 views

Mechanically proving element non-membership

I'm facing a (possibly simple) problem while proving a theorem. I need to show that under several (true) assumptions, some element is not in a set. Such assumptions are all met and there is are ...
• 543
87 views

What's so difficult about computer verifiable proofs?

What's so hard about creating a piece of software with as minimal as possible mathematical axioms, defining a formal language in which one can create new constructs based on the existing ones, and ...
• 119
37 views

Using the Fitch application and only Intro and Elim rules (& REIT if necessary), prove that $$\forall x \forall y (P(x) \implies Q(y)) \iff (\exists x P(x) \implies \forall y Q(y))$$ is a logical ...
1 vote
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 ...
1 vote
79 views

Time complexity of algorithms

I have some questions that I don't understand about time complexity. Given that the worst case complexity of the algorithm $A$ is $O(f(n))$ and the best case complexity of $A$ is $Ω(g(n))$. It ...
• 249
254 views

Is mutual inductive type definition essential in coq core language?

I'm studying Coq's core language and I found that mutual inductive type definition is in it. https://coq.inria.fr/refman/language/core/inductive.html#theory-of-inductive-definitions Before I read the ...
• 133
1 vote
163 views

Non-trivial difference(s) between Computer Algebra System and Proof Assistant

Disclaimer: I am not even an expert user of these two kinds of software. I understand that the trivial difference between proof assistants and CAS is that in proof assistants, the goal is to show that ...
• 111
117 views

What are the differences between LCF's Theorem and Automath's Prop?

How are the fundamental approaches to proving theorems by LCF and Automath different? Considering their modern descendants - Isabelle for LCF and Coq for Automath, both rely on type checking to do ...
1 vote
19 views

Does n^(1-1/d) always dominate log^d(n)

Hi I am currently learning about orthogonal range search and found two data structures with two different runtimes and wanted to proof that one always dominates the other. So I found out about k-d-...
688 views

What are the implications of Homotopy Type Theory?

I've recently come across the topic of homotopy type theory and I'm interested to learn more. I have a very limited background in type theory. Can anyone tell me, in functional programming terms or ...
288 views

Can every sentence of first-order logic be converted into an equisatisfiable equation in Boolean algebra?

There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational ...
163 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 ...
• 2,194
75 views

Difference between the logic and the type system of a proof assistant?

In Comparing Mathematical Provers (section 4.1), Wiedijk classifies logics and type systems of different proof assistants? I do not see what he means by type system of the assistant. He only says: A ...
• 2,194
4k views

How hard would it be to state P vs. NP in a proof assistant?

GJ Woeginger lists 116 invalid proofs of P vs. NP problem. Scott Aaronson published "Eight Signs A Claimed P≠NP Proof Is Wrong" to reduce hype each time someone attempts to settle P vs. NP. ...
• 325
1 vote
64 views

95 views

What does Dv mean in $F\star$ language?

In the $F\star$ tutorial it says Dv, the effect of a computation that may diverge; what does diverge mean here? It's not explained and it confuses me. I guess ...
• 940
603 views

Explanation of implication-introduction rule

I read in Proofs and Types by Girard et alii. the following excerpt that talks about the calculus of natural deduction: Now a sentence at a leaf (of the deduction tree) can be dead, when it no ...
• 2,194
461 views

What are the implications of Lean not having the type Set?

In Coq we have an impredicative base type, called Prop, and a predicative base type, called Set, both of type ...
• 485
729 views

How to Efficiently Define the Natural Numbers in Type Theory

A while ago I wondered about how Proof Assistants like Coq prove $m \leq n$ and the like. It looks like they actually need to traverse the natural numbers based on the successor/predecessor ...
• 2,223
577 views

Is Coq synthetic or analytic?

In CMU's HoTT course, lecture 1, which can be found here: https://scs.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=0945cc7f-48b7-4803-81af-e7193a3f461d At 33:52, Harper was giving parallel ...
• 632