Deduzione automatica

La deduzione automatica comprende la dimostrazione automatica di teoremi, per trovare prove di congetture, e la costruzione automatica di modelli, per trovare soluzioni di insiemi di vincoli. In deduzione automatica, la difficoltà del problema è spesso direttamente proporzionale all'espressività del linguaggio logico. La procedura di Apprendimento di Clausole Guidato da Conflitti, dall'inglese "Conflict-Driven Clause Learning" (CDCL), è una componente centrale dei sistemi per decidere la soddisfacibilità in logica proposizionale. Questa procedura limita le inferenze a quelle necessarie per spiegare i conflitti, e usa i conflitti per tagliare lo spazio di ricerca. Le attuali direzioni di ricerca in deduzione automatica vedono una convergenza verso l'obbiettivo di generalizzare questa nozione di soddisfacibilità guidata da conflitti dalla logica proposizionale alla logica del primo ordine, realizzando un paradigma di deduzione guidata da conflitti. Alcune direzioni di questo tipo si applicano al problema della soddisfacibilità modulo teorie in frammenti decidibili di teorie assiomatizzate in logica del primo ordine. In questo ambito la deduzione guidata da conflitti permette perfino una generalizzazione della classe dei problemi considerati da soddisfacibilità modulo teorie a soddisfacibilità modulo teorie e assegnamenti. Sviluppi non meno sorprendenti vedono l'applicazione della deduzione guidata da conflitti alla dimostrazione automatica di teoremi in logica del primo ordine. Queste direzioni di ricerca sono tanto promettenti quanto foriere di sfide entusiasmanti.