"Knowledge Base" system for the FO(·) language (first-order logic plus types, aggregates, inductive definitions, …). Reasoner is based on Z3.
IDP-Z3’s Reference Manual
Developed at Knowledge Representation and Reasoning @ KU Leuven