# Tag Info

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

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

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

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

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

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

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

### 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. ...
1 vote
Accepted

### What's the state of research on automated theorem proving?

I would suggest you to have a look at modern implementations of open source theorem provers frameworks, such as Lean and Coq. From there you can have a look into their bibliography to find relevant ...
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 ...
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 ...
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 ...

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