AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

-- Not specified --

Saarbrücken

Most automated reasoning systems operate on formulas in conjunctive normal form (CNF). However, standard CNF translation may result in exponential blow-up of the formula size. In 1968, Tseitin introduced a workaround for propositional logic which came to be known as Tseitin's encoding: sub-formulas of the overall formula are replaced by a single, fresh proposition, to escape repeated applications of the distributivity law and consequently obtain a shorter result, maintaining satisfiability. In 2001, Nonnengart and Weidenbach gave two important criteria for determining exactly which parts of a formula should be renamed. For first-order logic, we may employ one more significant enhancement: we can use one symbol to rename a set of consistent sub-formulas (sub-formulas that are instances of one general formula). We denote this by generalized renaming. Our work is the first to give a formal definition and solution of the problem of optimizing CNF translation using a sequence of generalized renamings. This talk gives an overview of the problem, underlying challenges, and solution.

--email hidden

passcode not visible

logged in users only