Leo-III - Paramodulation-Based Reasoning in HOL

deduction system for classical higher-order logic (HOL) is
developed. It aims at exploiting massive parallelism at
various levels in the reasoning process by employing independent
agents that are scheduled as optimization procedure using
combinatorical auction games. In its current state, Leo-III is
based on a paramodulation calculus for typed lambda-terms,
augmented with ordering constraints and special means of
extensionality treatment. HOL terms are represented as locally
nameless spine terms, together with perfect term sharing and
explicit substitutions. A key aspect of Leo's reasoning approach
is the cooperation with external specialist provers (most
prominently, but not limited to, first-order provers). In the talk,
we will survey the current state of the Leo-III prover and sketch
ongoing experiments and developments.