Re: Termination of resolution
- From: Panu Kalliokoski <panu.kalliokoski@xxxxxxxxxxx>
- Date: Wed, 08 Aug 2007 19:03:55 GMT
Chris Menzel wrote:
On Thu, 02 Aug 2007 10:46:53 +0300, Panu Kalliokoski
<panu.kalliokoski@xxxxxxxxxxx> said:
...
I know that resolution is undecidable in general (because it is a proof procedure for first order logic, whose proofs are undecidable),
I think you mean that the set of *theorems* of FOL is undecidable. It
is trivial to determine whether a sequence of formulas of FOL is a
proof.
Yes. Sorry for the unclear terminology.
Panu
.
- References:
- Termination of resolution
- From: Panu Kalliokoski
- Re: Termination of resolution
- From: Chris Menzel
- Termination of resolution
- Prev by Date: Re: Termination of resolution
- Next by Date: Re: Question: Given |X|>0 and |Y|>0, can X x Y be empty?
- Previous by thread: Re: Termination of resolution
- Next by thread: Re: Termination of resolution
- Index(es):
