Invited speakers:  

Workshop organisers: 

This workshop continues the series entitled "Proof Search in Type Theories" (PSTT at CADE'09, FLOC'10) and "Proof Search in Axiomatic Theories and Type Theories" (PSATTT at CADE'11).
Generic proofsearch in propositional and firstorder logic (even secondorder, higherorder) 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 proofsearch 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 theorybased 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 proofterm representations and dynamic proofterm construction during proofsearch,
• use of metavariables 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. deductionmodulo
• integration of domainspecific algorithms into generic deductive systems
• transformation of goals into particular shapes that can be treated by domainspecific 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 proofconstructing 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 tradeoff between completeness and efficiency,
• searching for proofs by induction, finding wellfounded 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.