[Haskell] Model vinden Propositie

[Glimi]

Het probleem:
Het vinden van alle modellen voor een opgebouwde Propositie boom binnen de functionele taal Haskell

Domein:
De definitie van een propositie:

Haskell:

data Prop
  = En [Prop] 
  | Of [Prop] 
  | Niet Prop
  | Prop :-> Prop -- (implicatie)
  | Var String    -- variabele
  | Bool Bool     -- constanten

Een propositie kan dus alleen opgebouwd worden uit conjuncties ( En ), disjuncties ( Of ), negaties (Niet), implicaties (:->), variabelen (Var) en contantes (Bool)
Hier is niets aan te veranderen.

Een propositie kan dus dingen zijn als

Haskell:

En( Var "a", Of( Niet (Var "b), Bool( True) ) )

Probleem:
Ik wil alle modellen hebben van deze expressie hebben. Een model zijn de waardes voor de variabelen zo, dat de expressie 'True' als waarde geeft

Overwogen:
• Brute force alle mogelijke waardes van de variabeles proberen. Dit werkt 100% zeker, maar is bloed traag
• Semantisch Tablaux loslaten op de expressie en door tegenstellingen ( a == fale en a == true in een tree) alle modellen te vinden. Dit wordt alleen ontzettend gecompileerd. Ik heb dan ook geen flauw idee hoe het te implementeren.

Kortom heeft iemand hier een idee voor om alle modellen van de expressie te vinden, of tips voor implementaties van het Tablaux? Verder ben ik ook nog aan het onderzoeken van Sequenten Calcus, dat schijnt makkelijk door machines gedaan te kunnen worden

Ik hoop dat iemand hier iets over kwijt wil Danku

[Pelle]

Dit moet in /14
Snap dat dan

Prutser

[marty]

Glimi schreef op 01 April 2003 @ 00:38:
Probleem:
Ik wil alle modellen hebben van deze expressie hebben. Een model zijn de waardes voor de variabelen zo, dat de expressie 'True' als waarde geeft

alle tautologiën bedoel je?
Dat red je ook met brute forcen niet volgens mij, want dat zijn er oneindig veel. Alleen al met implicatie en negatie kun je oneindig lange tautologiën maken.
Tenzij je natuurlijk alle tautologiën neemt die niet verder te vereenvoudigen zijn...
hmm...lastig. Valt dat niet in een logica boek terug te vinden ofzo?

[Pelle]

(btw, Glimi )

[Glimi]

marty schreef op 01 April 2003 @ 00:44:
alle tautologiën bedoel je?
Dat red je ook met brute forcen niet volgens mij, want dat zijn er oneindig veel. Alleen al met implicatie en negatie kun je oneindig lange tautologiën maken.
Tenzij je natuurlijk alle tautologiën neemt die niet verder te vereenvoudigen zijn...
hmm...lastig. Valt dat niet in een logica boek terug te vinden ofzo?

Nee bij een tautologie is ongeacht de waardes van variabelen de uitkomst van de Expressie in zijn geheel altijd true.

Ik wil dus voor een gegeven expressie (bijv ¬A v (B -> True) ) voor welke waardes van A en B de expressie naar true evalueerd
Da's een ander geval dan tautologien vinden

[marty]

ok, dan begreep ik je verkeerd (het voorbeeld wat je geeft is trouwens een tautologie )

Maar je wil dus voor een willekeurige propositie iets hebben wat aan de hand van die propositie zo'n model genereert?
Hmm..dat Semantisch Tableaux ken ik niet. Zou je me een linkje kunnen geven? Ben op zich wel nieuwsgierig wat dat is.
Maar is brute-forcen echt zo bloedje traag dan? Zolang een propositie niet ergens boven de 15 variabelen heeft valt dat toch best te doen? (dat geeft 32000 mogelijkheden)..

[RickN]

Volgens mij beschrijf je hier een moeilijker probleem dan het 3SAT probleem, en 3SAT is NP-compleet.

edit:
bij nader inzien, is dit gewoon het SAT probleem, en dat is dus ook NP-compleet.

[ Voor 36% gewijzigd door RickN op 01-04-2003 08:46 ]

[mbravenboer]

Een semantisch tableau opbouwen is minder lastig dan je waarschijnlijk denkt. Sterker nog: het kan prachtig uitgedrukt worden in een taal als Haskell.

De implementatie hiervan was vroeger een opdracht voor het vak "automatisch redeneren" op de UU. Toendertijd heb ik een implementatie in Java gemaakt, maar later heb ik het omgezet naar Stratego. De Stratego implementatie is zeer sterk te vergelijken met een implementatie in Haskell. Ik zou er dus gewoon voor gaan .

Eventueel kan hem wel online zetten, maar ik denk dat je beter zelf aan het prutsen kan gaan .

[ Voor 12% gewijzigd door mbravenboer op 01-04-2003 09:07 ]

[Verwijderd]

quote: mbravenboer

Een semantisch tableau opbouwen is minder lastig dan je waarschijnlijk denkt. Sterker nog: het kan prachtig uitgedrukt worden in een taal als Haskell.

De implementatie hiervan was vroeger een opdracht voor het vak "automatisch redeneren" op de UU.

Dat klopt, het implementeren van een waarheidschecker is nog steeds een onderdeel van äutomatisch redeneren". Hoewel, geloof ik, de opdracht tegenwoordig iets uitgebreider is dan vroeger...

quote: gimli

Verder ben ik ook nog aan het onderzoeken van Sequenten Calcus, dat schijnt makkelijk door machines gedaan te kunnen worden

Zoals mbravenboer ook al zegt is het implementeren van semantische tableux redelijk makkelijk. De methode die hij echter bedoelt is vrijwel vergelijkbaar met sequentencalculus, doordat je een linker en rechter sequent bijhoudt (je houdt bij welke "deel"-formules waar danwel onwaar moeten zijn).

Je kan dit in Haskell redelijk eenvoudig doen door twee lijsten bij te houden en volgens de regels van sequentencalculus de formules op te breken en naar links/rechts te verplaatsen.

Bijvoorbeeld de linker EN regel wordt iets als:

code:

breekFormule((EN [a,b]):restLijst,rechterLijst) = breekFormule(([a,b]++restLijst),rechterlijst)

De functie gebruikt nu de regel "\Gamma, A/\B ==> \Delta wordt \Gamma,A,B==>\Delta", en past dit toe door de EN aan de linkerzijde op te breken. Op vergelijkbare wijze kan je elementen van de linker naar de rechterlijst verplaatsen, en omgekeerd. Voor het splitsen van de afleiding moet je nog even iets slims verzinnen, en je moet even bedenken wanneer je nu klaar bent, en hoe je de waarden van de variabelen toewijst.

Ik heb het ooit vroeger (voor AR) zelf ook geimplementeerd, maar het is te lang geleden Bovendien heb ik toen Prolog gebruikt omdat ik dat een stuk makkelijker vond, maar in Haskell kan het net zo goed...

[Verwijderd]

Gimli, ken ik jou trouwens niet ergens van?

Toevallig dit jaar LV gedaan?

[mbravenboer]

Goh, gezellig thee-kransje zo .

[Verwijderd]

mbravenboer schreef op 01 April 2003 @ 10:30:
Goh, gezellig thee-kransje zo .

Zorg jij voor de cookies

[Verwijderd]

Goh, das ook toevallig, ik moet nu precies hetzelfde doen...

[Glimi]

marty schreef op 01 April 2003 @ 02:20:
ok, dan begreep ik je verkeerd (het voorbeeld wat je geeft is trouwens een tautologie )

Maar je wil dus voor een willekeurige propositie iets hebben wat aan de hand van die propositie zo'n model genereert?
Hmm..dat Semantisch Tableaux ken ik niet. Zou je me een linkje kunnen geven? Ben op zich wel nieuwsgierig wat dat is.

http://www.bath.ac.uk/~cs1spw/notes/CompIII/notes38.html

Maar is brute-forcen echt zo bloedje traag dan? Zolang een propositie niet ergens boven de 15 variabelen heeft valt dat toch best te doen? (dat geeft 32000 mogelijkheden)..

Mjah het wordt bloed traag ja, maar niet zo traag dat het niet werkbaar is in deze context. Punt is alleen de mooiheid he

mbravenboer schreef op 01 April 2003 @ 09:03:
Een semantisch tableau opbouwen is minder lastig dan je waarschijnlijk denkt. Sterker nog: het kan prachtig uitgedrukt worden in een taal als Haskell.

Ik denk dat het daarom ook de opdracht is

De implementatie hiervan was vroeger een opdracht voor het vak "automatisch redeneren" op de UU. Toendertijd heb ik een implementatie in Java gemaakt, maar later heb ik het omgezet naar Stratego. De Stratego implementatie is zeer sterk te vergelijken met een implementatie in Haskell. Ik zou er dus gewoon voor gaan .

Is nu dus een (beperkte) opdracht van Functioneel programmeren

Eventueel kan hem wel online zetten, maar ik denk dat je beter zelf aan het prutsen kan gaan .

Lijkt me logisch. Bovenal zijn scriptrequest verboden

Verwijderd schreef op 01 April 2003 @ 10:01:
Zoals mbravenboer ook al zegt is het implementeren van semantische tableux redelijk makkelijk. De methode die hij echter bedoelt is vrijwel vergelijkbaar met sequentencalculus, doordat je een linker en rechter sequent bijhoudt (je houdt bij welke "deel"-formules waar danwel onwaar moeten zijn).

Je kan dit in Haskell redelijk eenvoudig doen door twee lijsten bij te houden en volgens de regels van sequentencalculus de formules op te breken en naar links/rechts te verplaatsen.

Bijvoorbeeld de linker EN regel wordt iets als:

code:

breekFormule((EN [a,b]):restLijst,rechterLijst) = breekFormule(([a,b]++restLijst),rechterlijst)

Je voorbeeld is ontzettend duidelijk, het idee is me helder. Eigenlijk stom dat ik daar zelf niet opkwam

De functie gebruikt nu de regel "\Gamma, A/\B ==> \Delta wordt \Gamma,A,B==>\Delta", en past dit toe door de EN aan de linkerzijde op te breken. Op vergelijkbare wijze kan je elementen van de linker naar de rechterlijst verplaatsen, en omgekeerd. Voor het splitsen van de afleiding moet je nog even iets slims verzinnen, en je moet even bedenken wanneer je nu klaar bent, en hoe je de waarden van de variabelen toewijst.

Ik heb het ooit vroeger (voor AR) zelf ook geimplementeerd, maar het is te lang geleden Bovendien heb ik toen Prolog gebruikt omdat ik dat een stuk makkelijker vond, maar in Haskell kan het net zo goed...

Iig bedankt. Ik heb al een idee hoe dit aan te pakken en denk het redelijk simpel in elkaar te kunnen zetten zo.
Laat ik de oplossing maar niet posten hier, met al die aasgieren

Verwijderd schreef op 01 April 2003 @ 10:29:
Gimli, ken ik jou trouwens niet ergens van?

Toevallig dit jaar LV gedaan?

Ja vorig blok gehaald. Ik kan alleen u niet terugtraceren Dus toch wel Maar waar ben ik dan van bekend? Bij LV ben ik toch niet zo'n smart-ass geweest?

[Verwijderd]

Glimi schreef op 01 april 2003 @ 13:50:
[...]
Ja vorig blok gehaald. Ik kan alleen u niet terugtraceren

U? Zo formeel hoeft het nou ook weer niet.
Ik was werkgroepleider bij groep 4. Bovendien heb ik het tentamen afgenomen, vele vragen beantwoord (laatste werkcollege), de website verzorgt, e.d. Je zal me vast wel eens hebben gezien...

Dus toch wel Maar waar ben ik dan van bekend? Bij LV ben ik toch niet zo'n smart-ass geweest?

Je opmerking over sequentencalculus deed me vermoeden dat je LV had gedaan (daarnaast geeft je profiel aan dat je UU informaticus bent), het kon haast niet missen

[ Voor 26% gewijzigd door Verwijderd op 01-04-2003 13:59 ]

[mbravenboer]

Ik heb de opgave trouwens even doorgelezen ( hier dus). Het viel me op dat het nogal een mix is van vrij lastige tot volledig triviale vragen (nou ja, relatief dan ). De vrij lastige zijn echter weer vrij triviaal als je gewoon alle mogelijke bedelingen afloopt.

Is het dus wel de bedoeling dat je het met slimme methoden aan gaat pakken? (niet dat ik je daarvan wil weerhouden natuurlijk )

[Glimi]

Verwijderd schreef op 01 april 2003 @ 13:55:
U? Zo formeel hoeft het nou ook weer niet.
Ik was werkgroepleider bij groep 4. Bovendien heb ik het tentamen afgenomen, vele vragen beantwoord (laatste werkcollege), de website verzorgt, e.d. Je zal me vast wel eens hebben gezien...

Ja toen ik een foto vond op een website, wist ik genoeg Ik moet eigenlijk wel toegeven dat ik niet veel college's en werkcollege's heb meegemaakt

Je opmerking over sequentencalculus deed me vermoeden dat je LV had gedaan (daarnaast geeft je profiel aan dat je UU informaticus bent), het kon haast niet missen

Ow, dat 'kennen' in je vorige opmerking deed mij anders vermoeden Maar je bent geslaagd voor je detective-diploma

mbravenboer schreef op 01 april 2003 @ 14:03:
Ik heb de opgave trouwens even doorgelezen ( hier dus). Het viel me op dat het nogal een mix is van vrij lastige tot volledig triviale vragen (nou ja, relatief dan ). De vrij lastige zijn echter weer vrij triviaal als je gewoon alle mogelijke bedelingen afloopt.

Is het dus wel de bedoeling dat je het met slimme methoden aan gaat pakken? (niet dat ik je daarvan wil weerhouden natuurlijk )

Mjah creativiteit wordt toch gewaardeerd neem ik aan? Het heeft me iig nog nooit tegen gehouden om het anders te doen dan de bedoeling was (behalve bij één persoon dan )

[edit] De redding is nabij zie ik net Get Homework help NOW Check vooral de laatste zin

[ Voor 5% gewijzigd door Glimi op 01-04-2003 17:56 ]

[Glimi]

Uiteindelijke uitwerking

Ik heb er uiteindelijk voor gekozen om het simpel te houden. Omdat de grammatica alleen uit de conjunctie, disjunctie, implicatie, en de negatie bestond, kon het allemaal eigenlijk relatief simpel.

Ik heb er voor gekozen om eerst de propositie op 3 punten te versimpelen:
- Herschrijven implicatie naar ¬A v B
- Negatie doorvoeren tot de Leafs (Var's en Bools) dmv toepassen De Morgan
- Kortsluiten van conjuncties en disjuncties

In mijn versimpelde boom had ik dus slechts 3 datatypes en 2 operaties

Haskell:

data PropTree
   = EnNode [PropTree]
   | OfNode [PropTree]
   | NVarLeaf String
   | VarLeaf  String
   | BoolLeaf Bool

Stel dat ik nu een volgende propositie had staan:

Haskell:

Niet( En[ Var "a"
        , Bool True
        , Var "b" :-> Var "c"
        ] )

Laat zich herschrijven naar

Haskell:

Of[ Niet(Var "a")
  , Bool False
  , En [ Var "b"
       , Niet(Var "c")
       ]
  ]

Wat zich vertaalt in mijn syntax naar

Haskell:

OfNode[ NVarLeaf "a"
      , BoolLeaf False
      , EnNode [ VarLeaf "b"
               , NVarLeaf "c"
               ]
      ]

Bij het doorlopen op zoek naar oplossingen is het eigenlijk heel simpel.
Je begint onderaan en krijgt van de EnNode terug dat [VarLeaf "b", NVarLeaf "c"] waar moeten zijn (wat dus zegt dat "b" True moet zijn en "c" False)
Daarna wordt de OfNode behandeld. Deze voegt elke oplossing welke hij ontvangt van zijn kinderen samen in een lijst, terwijl de En ze combineerde

Kortom, antwoord hiervan zal zijn [ [VarLeaf "a"], [VarLeaf "b", NVarLeaf "c"] ], waarna je weet welke variabelen constraints hebben voor een oplossing.

Om het af te maken filter je dan nog de dubbele variabelen in 1 oplossing, filter je gelijke oplossingen, en filter je gesloten takken (takken met een VarLeaf en NVarLeaf met dezelfde naam).
Als je die oplossingen hebt, kan je gaan combineren met alle variabelen die in de propositie kunnen zitten.

Kortom hij is niet zo super mooi geworden als ik gehoopt had, maar werkt wel

Als afsluiting nog de uitwerking in Helium hier

code:

{- 
  Los een PropTree op. De gegeven oplossing zijn alle mogelijke oplossingen, niet gecontroleerd naar 
  tegenstellingen, dubbelen en niet aangevuld met variabelen die True/False mogen zijn..
  
  De oplossingen zien er als volgt uit
  [ [ "A", "B"], ["~Z", "P"], ["~A", "A"] ]
  Elke lijst binnen de lijst staat voor een mogelijke oplossing. 
  De eerste lijst [ "A", "B"] geeft aan dat een oplossing is als A en B waar zijn, de variabelen Z en P mogen zowel True als False zijn
  De tweede lijst ["~Z", "P"] geeft aan dat een oplossing is als Z False is en P True. De variabelen A en B mogen zowel True als False zijn
  De derde lijst ["~A", "A"] geeft aan dat A zowel True als False moet zijn. Dit is een gesloten boom.
-}                    
solveTableauxTree                     :: PropTree -> [ [PropTree] ]
solveTableauxTree (EnNode propTree')  = combineer $ map solveTableauxTree propTree
                                      where propTree = filter (not.isBoolLeaf) propTree'
solveTableauxTree (OfNode propTree')  = concatMap solveTableauxTree propTree
                                      where propTree = filter (not.isBoolLeaf) propTree'
solveTableauxTree var@(NVarLeaf _)    = [ [var] ]
solveTableauxTree var@(VarLeaf _)     = [ [var] ]
solveTableauxTree (BoolLeaf _)        = [ ]

{- 
  Combineer elk lijst in een lijst van lijsten met elkaar
  vb:
  combineer [ [ [ "a"], ["z"] ], [["q"], ["p", "g"] ] ] => [["a","q"],["a","p","g"],["z","q"],["z","p","g"]]
-}
combineer                            :: [ [[a]] ] -> [ [a] ]
combineer (x:xs)                     = [ x'++y | x' <- x, y <- (combineer xs) ]
combineer []                         = [[]]

Als u op/aanmerkingen heeft, roep ajb
Danku voor de aandacht

[Verwijderd]

Als u op/aanmerkingen heeft, roep ajb

Ik vraag me af of je algoritme wel veel efficienter is dan het simpel afgaan van al de bedelingen

Learning haskell by Helium

En wat vind je van Helium?

[Glimi]

Verwijderd schreef op 12 April 2003 @ 10:55:
Ik vraag me af of je algoritme wel veel efficienter is dan het simpel afgaan van al de bedelingen

Ik moet nog even precies nagaan in welke orde het algoritme van mij loopt ( er is me ook niet bekend of er een ticks functie is als in Hugs ), maar het testen op alle mogelijke opties zal minimaal 2n zijn.

En wat vind je van Helium?

Qua taal is het netjes hoor. Mooie foutmeldingen en betere rules qua identing dan Haskell
Jammer alleen dat het nog geen overloading heeft (of een overkoepelend type Num over Int en Float heen zou ook fijn zijn)

Als ik het goed zie is u trouwens de ontwikkelaar van Hint toch?