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


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

Reply via email to