Omega-ANTS

Ω-ANTS – An open approach at combining interactive and automated theorem proving. We present the $Omega$-ANTS theorem prover that is built on top of an agent-based command suggestion mechanism. The theorem prover inherits beneficial properties from the underlying suggestion mechanism such as run-time extendibility and resource adaptability. Moreover, it supports the distributed integration of external reasoning systems. We also discuss how the implementation and modeling of a calculus in our agent based approach can be investigated wrt. the inheritance of properties such as completeness and soundness.