|
ВИДЕОТЕКА |
Международная конференция «Logical Models of Reasoning and Computation»
|
|||
|
Deskolemization, equality and logical complexity Daniel Weller Vienna University of Technology |
|||
Аннотация: Skolemization is a well-known method to eliminate one type of quantifier from formulas and (cut-free) proofs. We are interested in questions about proof complexity (in the sense of logical complexity, i.e. the number of sequents in a proof): how much shorter can a proof of the Skolemization of F be when compared to proofs of F? We will show that in the presence of the equality schema, there exists an arbitrary speed-up. The result is proved using techniques from the generalization of proofs. Язык доклада: английский |