Skip to main content
Share Your Experience: Take the 2024 Developer Survey
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 ...
Joshua Grochow's user avatar
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 ...
Cris P's user avatar
  • 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}...
Andrej Bauer's user avatar
  • 29.1k
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 ...
Henning Basold's user avatar
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 ...
selig's 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 ...
D.W.'s user avatar
  • 12.1k
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 ...
cody's user avatar
  • 13.9k
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 ...
Neel Krishnaswami's 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 ...
hengxin's user avatar
  • 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 ...
cody's user avatar
  • 13.9k
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. ...
Neel Krishnaswami's user avatar
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 ...
Rexcirus's user avatar
  • 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 ...
MaiaVictor's user avatar
  • 3,137
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 ...
Gurkenglas's user avatar
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 ...
selig's user avatar
  • 333

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