dc.contributor.author | van den Broeck, Wim | |
dc.date.accessioned | 2023-01-12T00:32:58Z | |
dc.date.available | 2023-01-12T00:32:58Z | |
dc.date.issued | 2022-01-18 | |
dc.date.submitted | 2022-01-27T23:00:36Z | |
dc.identifier.uri | https://hdl.handle.net/11250/3042823 | |
dc.description.abstract | Any given propositional discourse can be expressed as a NAND-OR theory – a set of OR-clauses (disjunctions of literals) and NAND-clauses (negated conjunctions e.g. ¬(x∧y)) – making NAND-OR theories similar to traditional normal forms such as CNF and DNF. This thesis will discuss the inference system Neg; a non-explosive, sound and refutationally complete resolution system over NAND-OR theories. Of particular interest will be inconsistent theories which can be refuted in Neg by deriving the empty clause. The main result in this thesis will be a counterexample to the conjecture that the NAND-clauses of inconsistent NAND-OR theories need not grow greater than the size of its OR-clauses in the derivation of the empty clause. Further properties of such inconsistency derivations are explored with the aim of analysing the creation NAND-clauses in Neg. | |
dc.language.iso | eng | |
dc.publisher | The University of Bergen | |
dc.rights | Copyright the Author. All rights reserved | |
dc.subject | Proof complexity | |
dc.subject | Rneg | |
dc.subject | Neg | |
dc.subject | bounds | |
dc.subject | resolution | |
dc.subject | RIP | |
dc.title | Relative NAND-clause growth in Neg refutations | |
dc.type | Master thesis | |
dc.date.updated | 2022-01-27T23:00:36Z | |
dc.rights.holder | Copyright the Author. All rights reserved | |
dc.description.degree | Master's Thesis in Informatics | |
dc.description.localcode | INF399 | |
dc.description.localcode | MAMN-INF | |
dc.description.localcode | MAMN-PROG | |
dc.subject.nus | 754199 | |
fs.subjectcode | INF399 | |
fs.unitcode | 12-12-0 | |