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 ...
- 13.7k
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 ...
- 11.4k
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 ...
- 36.9k
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 ...
- 161
6
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}...
- 28.3k
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 ...
- 326
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 ...
- 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 ...
- 11.7k
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 ...
- 13.7k
3
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 ...
- 32.4k
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 ...
- 2,329
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 ...
- 13.7k
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. ...
- 32.4k
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 ...
- 244
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,117
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
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
Only top scored, non community-wiki answers of a minimum length are eligible