IDP-Z3: a reasoning engine for FO(.)

FO(.) (aka FO-dot) is a language that extends classical first-order logic with constructs to allow complex knowledge to be represented in a natural and elaboration-tolerant way. IDP-Z3 is a new reasoning engine for the FO(.) language: it can perform a variety of generic computational tasks using knowledge represented in FO(.). It supersedes IDP3, its predecessor, with new capabilities such as support for linear arithmetic over reals and quantification over concepts. We present four knowledge-intensive industrial use cases, and show that IDP-Z3 delivers real value to its users at low development costs: it supports interactive applications in a variety of problem domains, with a response time typically below 3 seconds.