Day 6: it's all about presentation
The best day so far at LPAR, with several really interesting talks on arithmetic, termination and complexity derivation, and first-order logic and theorem proving:
* Eugenia Ternovska on the logic PBINT: a logic that is designed to capture the complexity class NP, while at the same time providing features like built-in integer arithmetic that make it possible to encode practically relevant search problems in an elegant way. As I understand, the logic is tailored as an input language for answer-set programming ... definitely a paper that I need to study in more detail
* Georg Moser, Characterising Space Complexity Classes via Knuth-Bendix Orders: excellent talk on how the (seemingly) most hackish of all well-founded orders (Knuth-Bendix) has the surprising ability to capture space complexity classes (such as LINSPACE and PSPACE). Still puzzled why this happens to be the case for KBO, not for one of the more elegant orderings (such as lexicographic path orderings); need to ask Georg about this
* Christoph Sticksel, Labelled Unit Superposition Calculi for Instantiation-based Reasoning: the latest news on iProver and the integration of superposition
* Margus Veanes, Symbolic Automata Constraint Solving: quite an interesting talk on how to analyse strings, regular expressions, and context-free grammars using automata and SMT solvers. This is of very practical importance, since it can be used to detect (or verify the absence of) possible injection attacks in programs; an area of program verification that has become increasingly popular over the last few years
* Kai Bruennler, How to universally close the existential rule: Kai, the master of controversial research talks, presents ideas how to design sequent calculi for non-classical logics (such as first-order logic with possibly empty domain) in a more elegant way. In a nutshell, Kai believes that Skolem symbols introduced in proofs should be declared and bound explicitly in every sequent (using meta-quantifiers). Not quite sure I am completely convinced yet ;-) but certainly beautiful
Oh, and then there was the talk by this p2-r2 guy ;-)
Day 6: it's all about presentation
The best day so far at LPAR, with several really interesting talks on arithmetic, termination and complexity derivation, and first-order logic and theorem proving:
* Eugenia Ternovska on the logic PBINT: a logic that is designed to capture the complexity class NP, while at the same time providing features like built-in integer arithmetic that make it possible to encode practically relevant search problems in an elegant way. As I understand, the logic is tailored as an input language for answer-set programming ... definitely a paper that I need to study in more detail
* Georg Moser, Characterising Space Complexity Classes via Knuth-Bendix Orders: excellent talk on how the (seemingly) most hackish of all well-founded orders (Knuth-Bendix) has the surprising ability to capture space complexity classes (such as LINSPACE and PSPACE). Still puzzled why this happens to be the case for KBO, not for one of the more elegant orderings (such as lexicographic path orderings); need to ask Georg about this
* Christoph Sticksel, Labelled Unit Superposition Calculi for Instantiation-based Reasoning: the latest news on iProver and the integration of superposition
* Margus Veanes, Symbolic Automata Constraint Solving: quite an interesting talk on how to analyse strings, regular expressions, and context-free grammars using automata and SMT solvers. This is of very practical importance, since it can be used to detect (or verify the absence of) possible injection attacks in programs; an area of program verification that has become increasingly popular over the last few years
* Kai Bruennler, How to universally close the existential rule: Kai, the master of controversial research talks, presents ideas how to design sequent calculi for non-classical logics (such as first-order logic with possibly empty domain) in a more elegant way. In a nutshell, Kai believes that Skolem symbols introduced in proofs should be declared and bound explicitly in every sequent (using meta-quantifiers). Not quite sure I am completely convinced yet ;-) but certainly beautiful
Oh, and then there was the talk by this p2-r2 guy ;-)