Ω-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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element