Multirésolution pour le test de consistance et la déduction en logique propositionnelle
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
This thesis regards consistency and automatic deduction problems in propositional logic. The importance of experimentation'in a. I. Is first emphasized. Some criteria, allowing the improvement of the quality of comparisons are identified (transparency, objectivity, reproducibility, incrementality). The "satex" system take advantage of this criteria and use the web technologies to offer a satisfying experimental framework devoted to sat. Zfnc are introduced. This data structure extends the notion of binary decision diagrams to obtain a compact encoding of conjunctive normal form (cnf) formulae. Specialized operators are defined on zfnc, like the distribution between sets of clauses (clause-distribution). This allow the implementation of a new inference rule called "multiresolution", which extends the resolution principle and allow the cut elimination of variables on formulae with very large sets of clauses (only a compact representation of this set is maintained). Zres is an adaptation of the davis-putnam procedure (for satisfiability checking) based on multiresolution. The study of its properties, from a theoretical as well as from an experimental point of view, shows that it can solves some hard examples, such like the pigeon hole problem or urquhart problems, which are far beyond the scope of classical, resolution-based procedures. Zfnc's properties for deduction and knowledge-base compilation problems (prime implicates calculus, possibly restricted to some target language) are studied from a theoretical viewpoint. A very large experimental study shows that this new approach is not only appropriate to a large number of practical a. I. Applications but can push consequence-finding to a new limit, unreachable with explicit cnf representation.
Abstract FR:
Cette thèse concerne le problème de la consistance et de la deduction automatique en logique propositionnelle. L'importance de l'expérimentation en i. A. Est d'abord soulignée. Certains critères (transparence, objectivité, reproduction, incrémentalité) permettant d'améliorer la qualité des comparaisons sont identifiés. La plateforme "satex" reprend ces critères et utilise les technlogies du web pour offrir un cadre d'expérimentation satisfaisant, dédié au problème sat. Les zfnc sont ensuite introduits. Cette structure étend la notion de diagrammes binaires de décision (zbdd) pour obtenir une représentation compacte de formules sous forme normale conjonctive. Divers opérateurs spécialisés sont définis sur les zfnc, dont la distribution d'ensembles de clauses. Cela permet l'implémentation de la nouvelle règle d'inférence appelée "multirésolution", qui étend la resolution et permet l'élimination de variables par coupure, tout en travaillant sur des ensembles de clauses pouvant être exponentiellement grands (seule une représentation compacte de cet ensemble est maintenue). Zres est une reformulation de la procédure de davis et putnam pour le test de satisfiabilité, s'appuyant sur la multirésolution. L'étude de ses proprietes, tant au niveau théorique qu'expérimental, montre qu'il peut resoudre certains exemples jusqu'alors intraitables par les approches classiques basées sur la résolution, comme celui des pigeons (pigeon hole) ou ceux d'urquhart. Les propriétés des zfnc dans les problèmes de déduction et de compilation de base de connaissances (calculs d'impliqués premiers, éventuellement restreints a certains langages cibles) sont étudies de faÇon theorique. Une etude experimentale tres importante montre que cette approche est non seulement adaptee à un large spectre d'applications pratiques mais permet aussi de traiter des instances inabordables par les méthodes actuelles utilisant des représentations explicites.