Reasoners

Reasoners are software components or individuals that derive new information from a set of premises. In computer science and artificial intelligence, an automated reasoner applies rules of a formal logic or probabilistic model to determine whether certain statements follow from a knowledge base, to check consistency, or to generate plans.

Common types include: deductive reasoners that work with crisp logics such as first-order logic; forward-chaining rule engines and backward-chaining theorem provers; SMT solvers dealing with satisfiability modulo theories; and probabilistic reasoners that perform inference in Bayesian networks or Markov logic networks.

Reasoners used in knowledge representation and the semantic web apply ontologies. OWL reasoners (Pellet, HermiT, FaCT++) reason over RDF/OWL ontologies to infer class hierarchies, property characteristics, and inconsistencies.

Performance considerations: many logics are undecidable or have high worst-case complexity, so practical reasoners aim for sound but sometimes incomplete inference, trading completeness for scalability. Techniques include heuristics, approximations, modularization, and incremental reasoning. Inconsistent knowledge can pose challenges; some systems use paraconsistent approaches.

Applications include software verification, formal methods, data integration, intelligent agents, planning, and semantic search.

See also: automated theorem proving, constraint solving, ontology reasoning, semantic web.