2022 Developer Survey is open! Take survey.
19 votes
Accepted

Why is Proof Checker required in Proof Carrying Code

The purpose of the proof checker is to minimise the trusted computing base. By having a proof checker, neither the compiler nor the theorem prover need to be correct. The paper makes this point on ...
user avatar
14 votes
Accepted

Logical Reations for an Impredicative System in a Predicative MetaTheory

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent ...
user avatar
  • 13.1k
9 votes

What is the significance of nominal techniques?

Short answer. Formal reasoning about binding and $\alpha$-conversion with nominal approaches is closer to intuitive reasoning than alternative approaches. Longer answer. Binders arise everywhere in ...
user avatar
9 votes
Accepted

First order satisfiability that doesn't have finite models

Here's an amusing approach by Brock-Nannestad and Schürmann: Truthful Monadic Abstractions The idea is to try to translate first-order sentences into monadic first-order logic, by "forgetting" some ...
user avatar
  • 13.1k
8 votes
Accepted

Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem?

For Buchberger, it depends what you want it for, but generally speaking the answer is no. First, as pointed out on the Wikipedia article, the complexity upper bound given by Tarski-Seidenberg is ...
user avatar
8 votes
Accepted

What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

Principia Mathematica was a largely response to the various paradoxes discovered in mathematical logic at the turn of the 20th century. However the work itself, which has often been obliquely praised ...
user avatar
  • 318
8 votes

What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

Several points: As far as I know, Principia Mathematica uses essentially a formalization of set theory using a typed first order logic. It would therefore be tempting to use a first-order automated ...
user avatar
  • 13.1k
6 votes
Accepted

Which formalism is best suited for automated theorem proving in set theory?

There are numerous ways of formalizing set theory: ZFC uses first-order logic and a primitive relation $\in$ NBG uses first-order logic, a primitive relation $\in$, and a primitive predicate $S$ ...
user avatar
  • 26.4k
6 votes

How to determine whether a proof requires "higher-order reasoning techniques"?

Briefly, every theorem stated in first-order logic has a first-order proof. In his book "An Introduction to Mathematical Logic and Type Theory", Peter B. Andrews develops both first-order logic and a ...
user avatar
  • 161
6 votes
Accepted

Turing Machines as Coalgebras

Pavlovic et al. view Turing machines over a binary alphabet as coalgebras for the functor $\lambda X. \, 2 \times \mathcal{P}_{\mathrm{fin}}(X \times 2 \times \{\lhd,\rhd\})^2$. The symbols $\lhd$ and ...
user avatar
5 votes
Accepted

Extensional type theory and function extensionality

Yes, equality reflection and $\eta$-rule for functions together imply function extensionality. Recall that equality reflection is the rule $$\frac{\vdash p : \mathsf{Id}_A(a,b)}{\vdash a \equiv b : A}...
user avatar
  • 26.4k
3 votes
Accepted

Automatic theorem prover for first-order logic versus model checker

To add to the answer in the comments, it might help to first ask what the difference is between a model checker and an automated theorem prover for propositional logic. Given the statement $$p \wedge ...
user avatar
  • 333
3 votes
Accepted

If a root||nonce Proof-of-Work certificate is prime, can it be used in any other interesting proofs?

Heuristically: Yes, I suspect this probably works, if the system of equations is committed to in advance (well before mining works), and if the system of equations is small enough. You'll need the ...
user avatar
  • 10.3k
3 votes
Accepted

State of the Art for the Monadic Class?

I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS. In particular see the thesis of Ann-Christin Knoll, On Resolution Decision Procedures for ...
user avatar
  • 13.1k
3 votes

Automated theorem proving via unsupervised approaches

Here is a recent one: http://link.springer.com/chapter/10.1007%2F978-3-319-09284-3_17 You can get the fulltext here: http://arxiv.org/abs/1402.2184 It uses some state-of-the-art SAT solvers (see http:...
user avatar
2 votes

Looking for reference on NP-Completeness of proofs of length n

See this paper: On Godel’s Theorems on Lengths of Proofs II: Lower Bounds for Recognizing $k$ Symbol Provability by Samuel R. Buss, 1995. This paper discusses a claim made by Godel in a letter to ...
user avatar
  • 2,319
2 votes

Is there an algorithm to generate proof in Coq?

I guess the resource you are looking for is Adam Chlipala's Certified Programming with Dependent Types in which he builds up powerful tactics.
user avatar
  • 636
2 votes

State of the Art for the Monadic Class?

In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in Set Constraints are the Monadic Class. If memory serves, set constraints are ...
user avatar
2 votes

Automated proving that a program doesn't halt

In contradiction with Gurkenglas' answer, there actually is a community of scientists who work on proving non-termination of programs in various language and formalisms. An obvious approach would be ...
user avatar
  • 13.1k
2 votes

resolution based theorem prover for temporal logic

Your translation goes into Presburger arithmetic, which is decidable. You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. ...
user avatar
1 vote
Accepted

General Induction Principle

Can this formulation be trivially extended for each constructor by simply adding a Ci for an additional inductive case? Yes. I can't provide a general nor a technical answer, but a while ago I was ...
user avatar
  • 3,045
1 vote

Automated proving that a program doesn't halt

Since the Halting problem is undecidable, whatever approach I use to answer the question must eventually be unhelpful in the real world. There's a sequence of sets of programs such that each set is ...
user avatar
1 vote
Accepted

Formalized priority argument

Computability theory in general has been somewhat under-formalized. The short answer is that most theorems of computability theory do not pass one of the three tests for formalization: A proof that ...
user avatar
  • 13.1k
1 vote

Can we verify satisfiability of first order statements via saturation in sub-exponential time?

I am assuming by saturation you mean saturation-based reasoning as used by a resolution theorem prover e.g. where we negate and attempt to find a contradiction by saturation if we saturate we can ...
user avatar
  • 333
1 vote

Logic with Linear Programming

A nice book on this topic: "Optimization Methods for Logical Inference", V. Chandru, John N. Hooker, Wiley, 1999
user avatar
  • 191

Only top scored, non community-wiki answers of a minimum length are eligible