Questions tagged [proof-assistants]

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

16 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
10
votes
0answers
309 views

Is Agda sound as a proof system?

I was browsing Agda's stdlib source code, since I was trying to get into it seriously and therefore wanted to know more. I was amazed at that Agda is way more developed than I thought and it's ...
5
votes
0answers
59 views

Can we simulate any dependent datatype with `Eq`?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
3
votes
0answers
56 views

A book introducing proof theory needed (many-sorted FOL, classical non-Gentzen calculus, satisfiability in partial algebras, induction)

We define a signature as a triple $$\Sigma\ =\ (S,F,\mathrm{type})$$ where $S$ is a set of sorts, $F$ a set of $n$-ary function symbols $f$ of the type $\mathrm{type}(f)$ $=$ $(M_1,\dotsc,M_n\...
2
votes
0answers
44 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?
2
votes
0answers
50 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 ...
2
votes
0answers
29 views

How does supercompilers relate to macro tree transducers?

Supercompilers can be used as a generalisation of deforestation of a functional program. Macro Tree Transducers composition can be used to the same effect, using a completely different approach. What ...
1
vote
0answers
57 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$ . ...
1
vote
0answers
24 views

Good Reference For Design And implementation Of Proof-Assistant

Hello I'm searching for any good review article or book about the design an implementation of a proof-assistant, something such as the Dragon book for programming language. My background is ...
1
vote
1answer
113 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) ...
1
vote
0answers
80 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 ...
1
vote
0answers
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 ...
0
votes
0answers
29 views

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 ...
0
votes
0answers
13 views

How to check an formula is an instance of axiom schema with $\lambda$-Prolog?

I want to make a proof assistant for First-Order Logic which can deal with axiom schema. I have implemented a little bit, and the $\lambda$-Prolog code is under the below. I have already defined an ...
0
votes
0answers
100 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 ...
0
votes
0answers
24 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: ...
0
votes
0answers
44 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 -...