Questo sito utilizza cookies, anche di terze parti, per mostrare pubblicità e servizi in linea con il tuo account. Leggi l'informativa sui cookies.
Username: Password: oppure
C/C++ - Algoritmo di risoluzione di Robinson
Forum - C/C++ - Algoritmo di risoluzione di Robinson

Avatar
Dice (Normal User)
Expert


Messaggi: 238
Iscritto: 26/11/2011

Segnala al moderatore
Postato alle 12:16
Domenica, 25/03/2012
Non sapevo se mettere questa discussione nella sezione dell'ANSI C o del PROLOG, ma intanto la scrivo qua:

avrei bisogno che mi spiegaste in dettaglio come funziona l'algoritmo di risoluzione di Robinson, e anche qualche pratico consiglio su come implementarlo in ANSI C.

Thank you very much :k:


La vita è un biscotto ma se piove si scioglie !!!
PM Quote
Avatar
Il Totem (Admin)
Guru^2


Messaggi: 3635
Iscritto: 24/01/2006

Segnala al moderatore
Postato alle 20:00
Martedì, 27/03/2012
E' semplicemente il principio di risoluzione usato in logica proposizionale. Qui puoi trovarne una descrizione:
http://www.ce.unipr.it/research/HYPERPROLOG/clausris.html
A dispetto della definizione, è abbastanza intuitivo. Altri principi di risoluzione sono applicabili, sebbene siano indecidibili, anche alla logica del prim'ordine e a logiche più ampie.


"Infelici sono quelli che hanno tanto cervello da vedere la loro stupidità."
(Fligende Blatter)

"Dubitare di se stessi è il primo segno d'intelligenza."
(Ugo Ojetti)
PM Quote
Avatar
Dice (Normal User)
Expert


Messaggi: 238
Iscritto: 26/11/2011

Segnala al moderatore
Postato alle 0:02
Giovedì, 29/03/2012
Grazie mille, adesso ho capito come funzione Robinson;
adesso però ho un piccolo problema: ho fatto un programma che mi acquisisce l'insieme delle clausole, però quando vado a chiedere all'utente quali insiemi di clausole vuole considerare non so come fare; adesso vi faccio vedere quello che ho fatto:

int main (void)
{
    char    *insieme_clausole;    /*vettore contenente la formula inserita*/
    int    i,            /*indice del vettore formula*/
        carattere_letto,    /*variabile per memorizzare la formula*/
        conta_clausole = 0,    /*contatore delle clausole*/
        numero_clausola;    /*numero indivativo delle clausole*/

    /*allocazione dinamica*/
    insieme_clausole = (char *) malloc(sizeof (char)*100);

    
    /*inserimento insieme di clausole*/
    printf("Inserisci la formula:\n\n");
    printf("-> ");
    /*acquisizione insieme di clausole*/
    for(i = 0;
        ((carattere_letto = getchar()) != '\n');
        i++)
        insieme_clausole = carattere_letto;
    /*inserisco il carattere di terminazione*/
    insieme_clausole = '\0';
    printf("\n");

    /*stampa l'insieme di clausole*/
    printf("L'insieme di clausole è: %s\n",
           insieme_clausole);

    /*contare quante clausole ci sono*/
    for(i = 0;
        (insieme_clausole != '\0');
        i++)
        if(insieme_clausole == '}')
            conta_clausole++;
    printf("Le clausole sono: %d\n",
           conta_clausole - 1);

    /*adesso devo prendere le clausole considerate*/
    printf("Quali clausole vuoi considerare (indicarle con i numeri decimali separati da virgole):\n\n");
    printf("-> ");




Per farvi capire meglio vi faccio un esempio di quello che io VORREI CHE FACCIA:
inserisci le clausole: {{p,!q,r},{!p},{q},{!r}}
quali clausole vuoi considerare: 1,2
le clausole considerate sono: {p,!q,r},{!p}
la risolvente è:{!q,r}

Come posso fare per fargli acquisire sole le clausole che mi indica l'utente?


La vita è un biscotto ma se piove si scioglie !!!
PM Quote
Avatar
Dice (Normal User)
Expert


Messaggi: 238
Iscritto: 26/11/2011

Segnala al moderatore
Postato alle 1:31
Lunedì, 02/04/2012
Niente eh ?

Babba bia:-o:noway:


La vita è un biscotto ma se piove si scioglie !!!
PM Quote
Avatar
Il Totem (Admin)
Guru^2


Messaggi: 3635
Iscritto: 24/01/2006

Segnala al moderatore
Postato alle 10:30
Martedì, 03/04/2012
Perché semplicemente non risolvi sulle clausole inserite?


"Infelici sono quelli che hanno tanto cervello da vedere la loro stupidità."
(Fligende Blatter)

"Dubitare di se stessi è il primo segno d'intelligenza."
(Ugo Ojetti)
PM Quote
Avatar
Dice (Normal User)
Expert


Messaggi: 238
Iscritto: 26/11/2011

Segnala al moderatore
Postato alle 0:15
Venerdì, 06/04/2012
Cosa intendi ?
Spiega in dettaglio please


La vita è un biscotto ma se piove si scioglie !!!
PM Quote
Avatar
Il Totem (Admin)
Guru^2


Messaggi: 3635
Iscritto: 24/01/2006

Segnala al moderatore
Postato alle 8:22
Martedì, 17/04/2012
Semplicemente richiedi le sole clausole di cui intendi calcolare il risolvente.


"Infelici sono quelli che hanno tanto cervello da vedere la loro stupidità."
(Fligende Blatter)

"Dubitare di se stessi è il primo segno d'intelligenza."
(Ugo Ojetti)
PM Quote
Avatar
aleandro03 (Normal User)
Newbie


Messaggi: 15
Iscritto: 20/05/2013

Segnala al moderatore
Postato alle 16:02
Lunedì, 20/05/2013
Ciao avrei bisogno di aiuto con l'implementazione di Robinson in C, qualcuno può aiutarmi?

PM Quote