# Questions tagged [proof-assistants]

Applications that allow to create formal proofs. They assist the user by finding partial and checking complete proofs.

64 questions
Filter by
Sorted by
Tagged with
48 views

### What's the problem of Learning Algorithms used for Automated Theorem Provers?

I've googled a lot but I haven't found an automated theorem prover/problem solver able to solve problems like a human. I am interested in a specific type of prover: the learning ones, like Support ...
32 views

### Can someone pelase give a counter example of it? If a problem is in NP then there is no known polynomial time algorithm to solve it

Is there any known polynomial time algorithm to solve a problem which that problem is in NP. I was told is False but can't think of any counter example now.
77 views

### How to remove a universal quantifier in Lean theorem prover

I am working with two binary relations: g_o and pw_o, and I've defined pw_o below: constants {A : Type} (g_o : A → A → Prop) ...
51 views

### Prove that grammar $S \to aSc | \epsilon | bBc$ ,$B \to bBc | \epsilon$ generates language $\{a^ib^jc^{i+j} | i,j \ge 0 \}$

Prove that grammar $G$ with productions: $S \to aSc|\epsilon | bBc$ $B\to bBc | \epsilon$ Generates language $L = \{a^ib^jc^{(i+j)}$ | $i,j \ge 0 \}$ Step 1. Prove $L(G) \subseteq L$ . ...
22 views

### Structural induction a particular case of (co)induction rule of an inductive predicate

What is the relation between the principle of induction on terms: ...
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 ...
201 views

33 views

### The underlying type theory of HOL/Isabelle

Is there a good source on the type theory of HOL/Isabelle/other HOL-based LCF-style theorem provers?
32 views

### Computational type theorists: how do you compare terms for equality here?

I am attempting to implement Simple Type Theory in the language D. How do you compare subterms to a term $R$ for the sake of computing the covering abstractors of $R$ in $M$? By reference (class ...
170 views

### Why cannot match $Bool \equiv Bool$ with $refl$ while $1 \equiv 1$ can?

This code depends on agda-stdlib: ...
177 views

### How to prove this obvious theorem in type theory (LEAN prover)

I have the following code: ...
55 views

277 views

### Is it possible to implement dependent types by any object oriented language supporting inheritance and classes?

When I was reading Agda tutorial, I noticed resemblance between dependent type declarations and class definitions which I've been primarily used to work with. I'm not totally sure how much sense this ...
54 views

### Number of words in $L$ of length $n$?

Be $L$ a formal language over the alphabet $\Sigma$. $L$ can be defined by induction: $L^0 = \{\epsilon\}$ and for $i>0: L^i = \Sigma*L^{i-1}$. Means that $|L^n|$ is the number of words in $L$ of ...
2k views

### Recursive definitions over an inductive type with nested components

Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...
74 views

### Universal theorem proving algorithms for sequent calculus (e.g. for cut-free logics)?

Some of the logics admit Gentzen-style sequent calculus. Are there universal algorithms that allow to find proof (derivation of the proof) in sequent caculus for every hypthetical theorem? Some of ...
276 views

### How come identity encodes absurdity

From P5 in this paper: https://hal.inria.fr/hal-01094195/file/CIC.pdf Using this purely functional part, it is possible to encode many int eresting notions. For instance ∀ C : Prop , C ...
150 views

### Is Goedel's 1st theorem not algorithmically derivable?

First let me explain what I mean by algorithmically derivable. An algorithm must be able to come up with the proof without prior knowledge of the proof, in the same way mathematicians and computer ...
153 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 ...
113 views

### Can a type system serve as a proof assistant for foreign functions?

Given that: A language with very expressive type systems (e.g. Idris) can also have escape mechanisms like foreign function interfaces/unsafePerformIO. There are proof assistants that can be used to ...
700 views

### What is a quotient structure?

I was reading a paper here, and it mentioned "quotient structure" in the following sentence (third page, second paragraph of the paper) In order to obtain a representation of terms truly isomorphic ...
73 views

### Explanation of proof of why connectedness is not conjunctively local of any order $k$

I was reading Minsky's and Papert's book on perceptrons and I was reading theorem 0.6.1 and I was having a hard time understanding it. The theorem was about proving that the property "connected" was ...
199 views

### Is there a fundamental reason/limitation, such as $P \not = NP$, that prevents computers from being able to do mathematics (proofs, etc.)?

I'm a student, so I apologise if this is an idiotic question: Is there a fundamental reason/limitation, such as $P \not = NP$, that prevents computers from being able to do mathematics (posing ...
356 views

### How would one prove the pigeonhole principle with a SAT solver?

Suppose I wanted to find a proof of the pigeonhole principle or show that no proof shorter than $L$ exists. I understand that proof-checking is in NP, so I could write a CNF formula that is ...
53 views

### Use of Mizar for algorithm specification and automatic analysis and discovery of algorithms?

Is it possible to use Mizar Mathematical Library for the specification of algorithms at the same detalization level as the implementation of the algorithm in industrial programming language? Mizar ...
40 views

### How far meta-logical frameworks are from universal logic?

I am investigating metalogical-frameworks like Isabelle/Pure (very few information), http://twelf.org/wiki/Main_Page, http://abella-prover.org/ for encoding of new logics. And natural question arises -...
63 views

### Tool for generating all the consequences of the logical theory (general logic programming framework)?

I am reading article https://arxiv.org/pdf/cs/0511055v1.pdf (about defeasible deontic logic) and it mentions on page 10 the operator T that constructs extension (set of immediate consequences) from ...
48 views

### How to lexically list sentences in peano arithmetic?

I am working on building a toy automated theorem prover, What I want to do is to efficiently generate sentences in peano arithmetic, that I can attempt to verify as True/False/requires-more-resources ...
140 views

### Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
58 views

### Can we simulate any dependent datatype with Eq?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
465 views

### Can we prove mathematical induction statements in Lisp?

My previous question Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program? has a problem that it tries to cover too much ground. Here is a related question motivated by ...
290 views

### Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...