2022 Developer Survey is open! Take survey.

# Tag Info

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 ...
• 10.3k
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 ...
• 13.1k

### 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 ...
• 10.3k
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 ...
• 13.1k
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 ...
• 35.6k
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 ...
• 318

### 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 ...
• 13.1k
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$ ...
• 26.4k

### 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 ...
• 161
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 ...
Accepted

• 333
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 ...
• 10.3k
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 ...
• 13.1k

### 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:...

### 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 ...
• 2,319

### 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.
• 636

### 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 ...
• 31.6k

### 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 ...
• 13.1k

### 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. ...
• 31.6k
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 ...
• 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 ...
• 113
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 ...
• 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 ...
• 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
• 191

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