http://stackoverflow.com/questions/6571200/pilog-assertion

## Advertising

On Mon, Jul 04, 2011 at 12:26:46AM -0700, Doug Snead wrote:
> Consider these five pilog assertions.
>
> (be do ((Question @P) @S @S) (holds @P @S))
>
> (be holds (@A @S)
> (restoreSitArg @A @S @F)
> (2 cons (-> @F)))
>
> (be On (3 s0))
> (be On (5 s0))
>
> (be restoreSitArg ((On @N) @S (On @N @S)))
>
> I define some tests.
>
> (de t_1 () # ok
> (? holds On restoreSitArg (holds (On @N) s0)) )
>
> (de t_2 () # ?
> (? do holds On restoreSitArg (do (Question (On @N)) s0 s0)) )
>
> Run the first one.
>
> (t_1)
> 1 (holds (On @N) s0)
> 1 (restoreSitArg (On @N) s0 (On @N s0))
> 1 (On 3 s0)
> @N=3
> 2 (On 5 s0)
> @N=5
> -> NIL
>
> Ok, in that first test, I asked for solutions to (holds (On @N) s0)), tracing
> on.
>
> Those are solutions I would expect, and they are correct.
>
> Second test.
>
> (t_2)
> 1 (do (Question (On @N)) s0 s0)
> 1 (holds (On @N) s0)
> 1 (restoreSitArg (On @N) s0 (On @N s0))
> 1 (On 3 s0)
> @N=NIL
> 2 (On 5 s0)
> @N=NIL
> -> NIL
>
> Now here, (holds (On @N) s0) is also attempted to be proved - because it is a
> sub-goal of (do (Question (On @N)) s0 s0).
>
> My question is, why the difference when (holds (On @N) s0) is proved?
>
> In one case solutions are found, in the other case it seems to miss the same
> solutions to the same goal.
>
> Cheers,
>
> Doug
>
> --
> UNSUBSCRIBE: mailto:picolisp@software-lab.de?subject=Unsubscribe
--
UNSUBSCRIBE: mailto:picolisp@software-lab.de?subject=Unsubscribe