Dear Dmitry, To make things clearer: Mozart is not a theorem prover. It doesn't know about logic rules like modus ponens, etc. The constraint solver may help you to find solutions to some logic problem within some finite domain. You can also check whether a given property is true (within a finite domain) by searching solutions to its negation, i.e., counter-examples. But the existing Mozart libraries do not go beyond that...
I hope it helps, Raphael On Tue, Aug 18, 2009 at 10:47 AM, Dmitry Negius <[email protected]> wrote: > Anders you nearly completely answer my question with one exception. > From your translation I see that negation and implication are supported > in the constraints specification. But... > > 2009/8/18 Torsten Anders <[email protected]> > >> Dear Dmitry, >> >> I don't quite understand your system, do you mean a constraint problem >> like the following? >> >> {Browse >> {SearchOne >> proc {$ Sol} >> %% variable domain declaration >> A = {FD.decl} >> B = {FD.int 0#1} >> in >> Sol = unit(a:A b:B) >> %% constraint application >> A <: 1000 >> {FD.impl (A >: 255) B 1} > > (1) > >> >> {FD.impl {FD.nega B} {FD.nega (A >: 255)} 1} > > (2) > > Above clause (2) can be infered from the clause (1) by the modus ponens > rule. > Can Mozart-Oz interpreter infer clause (2) from clause (1) automatically ? > > >> >> %% and so forth >> %% >> %% distribution strategy (variable ordering) >> {FD.distribute ff Sol} >> end}} >> >> Best >> Torsten >> >> >> On Aug 17, 2009, at 6:58 PM, Dmitry Negius wrote: >> >>> Excuse me but I want to ask: "Does mozart-oz solves logicaly-algebral >>> constraints - the mix of logical and algebral operations over variables? >>> System NUT for example solves only algebral constraints in the form of >>> algebraic equations (formula = formula). >>> >>> For my AI project I need to solve constraints like this: >>> A>255 => B. >>> not B. >>> ?- A<1000. >>> >>> Of couse this is mo intelligent then to solve only algebraic constraints >>> and has better application. >>> >>> Manually this constaints system can be solved in the next way: >>> >>> A>255 => B >>> ------------------- >>> not B => not (A>255) >>> ------------------------------- >>> not B => (A=<255) not B >>> ---------------------------------------------------- >>> A=<255 >>> 255<1000 >>> ------------------------- >>> A<1000 >>> >>> >>> >>> -- >>> Torsten Anders >>> Interdisciplinary Centre for Computer Music Research >>> University of Plymouth >>> Office: +44-1752-586219 >>> Private: +44-1752-558917 >>> http://strasheela.sourceforge.net >>> http://www.torsten-anders.de >>> >>> >>> >> _________________________________________________________________________________ >> mozart-users mailing list >> [email protected] >> http://www.mozart-oz.org/mailman/listinfo/mozart-users >> > > > > -- > Normal people grows o...@# > > > _________________________________________________________________________________ > mozart-users mailing list > [email protected] > http://www.mozart-oz.org/mailman/listinfo/mozart-users >
_________________________________________________________________________________ mozart-users mailing list [email protected] http://www.mozart-oz.org/mailman/listinfo/mozart-users
