Le compilateur br2cnf est un programme permettant de compiler une instance de révision de croyance CNF donnée en une formule CNF équivalente. Plusieurs opérateurs de révision de croyance basés sur la distance décomposable par sujet ont été implémentés, notamment ceux basés sur la distance drastique ou la distance de Hamming entre les interprétations, et utilisant la somme, leximin ou leximax comme fonction d’agrégation.


Auteurs :
Sébastien Konieczny
Pierre Marquis
Jean-Marie Lagniez

Toute catégorie    Compilateurs   

Aller sur la page web du logiciel

Chapitres d'ouvrages

2017 Sébastien Konieczny, Jean-Marie Lagniez, Pierre Marquis, Boosting Distance-Based Revision Using SAT Encodings in Logic, Rationality, and Interaction, vol. 10455, pp. 480-496, Springer Berlin Heidelberg, 2017.