Broadly v iewed, Craig Interpolation (CI), Beth Definability (BD), and Second-Order Quantifier Elimination (SO QE) concern the existence and computation of formu las that capture consequences or logical constrain ts under some syntactic restrictions. Since such e xistence/computation questions arise in many areas of computer science, CI, BD, and SOQE have been t horoughly investigated by different communities, w hich has led to a large number of results, from fo undational issues to practical applications. Relev ant fields include proof theory, model theory, pro of complexity, automated reasoning, automata theor y, knowledge representation, program verification and databases as well as philosophy and linguistic s.
\nThe aim of the workshop is to bring t ogether researchers from the many relevant fields to exchange experiences and findings about approac hes, techniques, ongoing research and important op en problems. We strongly believe that CI, BD, and SOQE – beyond sharing a similar historical backgro und – offer a common basis for fruitful cross-disc iplinary exchange.
\nCI-BD-SO QE continues a series of previous workshops on Cra ig Interpolation, Beth Definability, and Second-Or der Quantifier Elimination. Contributions shall be in the form of original research (full papers or extended abstracts) and abstracts of previously pu blished research. If selected, at least one author is expected to present their work in person at th e conference.
\n