International Workshop on
Proof-Search in Axiomatic Theories and Type Theories

This workshop continues the series entitled "Proof Search Type Theories" (PSTT at CADE'09, FLOC'10), and enlarges its scope to encompass proof search in axiomatic theories as well.

Generic proof-search in propositional and first-order logic (even second-order, higher-order) are fields that already benefit from a long research experience, spanning from techniques as old as unification to more recent concepts such as focusing and polarisation.

More adventurous is the adaptation of generic proof-search mechanisms to the specificities of particular theories, whether these are expressed in the form of axioms or expressed by sophisticated typing systems or inference systems.

The aim of this workshop is to discuss proof search techniques when these are constrained or guided by the shape of either axioms or inference/typing rules. But it more generally offers a natural (and rather informal) venue for discussing and comparing techniques arising from communities ranging from logic programming to type theory-based proof assistants, or techniques imported from the fields of automated reasoning and SMT but with an ultimate view to build proofs or at least provide proof traces.

TOPICS:
Papers are solicited on topics including, but not limited to:
• invertibility of deductive rules, polarity of connectives and focusing devices,
• more generally, development and application of theorems establishing the existence of normal forms for proofs,
• explicit proof-term representations and dynamic proof-term construction during proof-search,
• use of meta-variables to represent unknown proofs to be found,
• use of failure and backtracking in proof search,
• integration of rewriting or computation into deductive systems, as organised by e.g. deduction-modulo
• integration of domain-specific algorithms into generic deductive systems
• transformation of goals into particular shapes that can be treated by domain-specific tactics or external tools
• externalisation of some proof searching tasks and interpretation of the obtained outputs (justifications, execution traces...)
• more generally, interfaces between cooperating tools
• importation of automated reasoning techniques and SMT techniques to proof-constructing frameworks
• quantifier instantiation in SMT techniques, arbitrary alternation of forall/exists quantifiers
• unification in particular theories or in sophisticated typing systems

More generally, contributions about the following topics are welcome
• proof search strategies, their complexity and the trade-off between completeness and efficiency,
• searching for proofs by induction, finding well-founded induction measures, strengthening goals to be proved by induction, etc,
• reasoning on syntaxes with variable binding (in e.g. quantifiers or data structures),
• termination, computational expressivity of related programming paradigms,
• user interaction and interfaces,
• systems implementing any of the ideas described above. Synthesising some of the above aspects into unifying theories is a concern of our research theme that aims at bringing together research efforts of different communities, enhancing their interaction. Contributions made in a spirit of synthesis are thus particularly welcome.

PSATTT'11 is supported by:s