C/C++ - Algoritmo di risoluzione di Robinson

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

E' semplicemente il principio di risoluzione usato in logica proposizionale. Qui puoi trovarne una descrizione:
ce.unipr.it/research/HYPERPROLOG/…
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.

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[i] = carattere_letto;
    /*inserisco il carattere di terminazione*/
    insieme_clausole[i] = '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[i] = carattere_letto;
    /*inserisco il carattere di terminazione*/
    insieme_clausole[i] = '{parsed_message}';
    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[i] != '{parsed_message}');
     i++)
        if(insieme_clausole[i] == '}')
            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?';
    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[i] != '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[i] = carattere_letto;
    /*inserisco il carattere di terminazione*/
    insieme_clausole[i] = '{parsed_message}';
    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[i] != '{parsed_message}');
     i++)
        if(insieme_clausole[i] == '}')
            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?');
     i++)
        if(insieme_clausole[i] == '}')
            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?

Niente eh ?

Babba bia

Perché semplicemente non risolvi sulle clausole inserite?

Cosa intendi ?
Spiega in dettaglio please

Semplicemente richiedi le sole clausole di cui intendi calcolare il risolvente.

Ciao avrei bisogno di aiuto con l'implementazione di Robinson in C, qualcuno può aiutarmi?