Ω-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
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Benzmüller, Christoph; Sorge, Volker; Jamnik, Mateja; Kerber, Manfred: Combined reasoning by automated cooperation (2008)
- Wagner, Marc; Autexier, Serge; Benzmüller, Christoph: \textscPlat(\Omega): a mediator between text-editors and proof assistance systems (2007)
- Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with (\Omega)MEGA (2006)
- Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
- Siekmann, J.; Benzmüller, C.; Fiedler, A.; Meier, A.; Pollet, M.: Proof development with (\Omega)MEGA: (\sqrt2) is irrational (2002)
- Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Distributed assertion retrieval (2001)
- Benzmüller, Christoph; Sorge, Volker: (\Omega)-ANTS -- An open approach at combining interactive and automated theorem proving (2001)
- Jamnik, Mateja; Kerber, Manfred; Benzmüller, Christoph: Towards learning new methods in proof planning (2001)
- Kerber, Manfred (ed.); Kohlhase, Michael (ed.): Symbolic computation and automated reasoning. The CALCULEMUS-2000 symposium. 8th symposium on the integration of symbolic computation and mechanized reasoning, St. Andrews, Scotland, GB, August 6--7, 2000 (2001)