Omega: Towards a Mathematical Assistant. - Christoph Benzmüller; Lassaad Cheikhrouhou; Detlef Fehrer; Armin Fiedler; Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Karsten Konrad; Andreas Meier 002; Erica Melis; Wolf Schaarschmidt; Jörg H. Siekmann; et al. (CADE, 1997)

L<Omega>UI: Lovely <Omega>MEGA User Interface. - Jörg H. Siekmann; Stephan M. Hess; Christoph Benzmüller; Lassaad Cheikhrouhou; Armin Fiedler; Helmut Horacek; Michael Kohlhase; Karsten Konrad; Andreas Meier 002; Erica Melis; Martin Pollet; Volker Sorge (Formal Aspects Comput., 1999)

System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. - Andreas Meier 002 (CADE, 2000)

Proof Planning with Multiple Strategies. - Erica Melis; Andreas Meier 002 (Computational Logic, 2000)

Classifying Isomorphic Residue Classes. - Andreas Meier 002; Martin Pollet; Volker Sorge (EUROCAST, 2001)

Employing Theory Formation to Guide Proof Planning. - Andreas Meier 002; Volker Sorge; Simon Colton (AISC, 2002)

Proof Development with OMEGA. - Jörg H. Siekmann; Christoph Benzmüller; Vladimir Brezhnev; Lassaad Cheikhrouhou; Armin Fiedler; Andreas Franke 001; Helmut Horacek; Michael Kohlhase; Andreas Meier 002; Erica Melis; Markus Moschner; Immanuel Normann; et al. (CADE, 2002)

Proof Development with Omega-MEGA: sqrt(2) Is Irrational. - Jörg H. Siekmann; Christoph Benzmüller; Armin Fiedler; Andreas Meier 002; Martin Pollet (LPAR, 2002)

Comparing Approaches to the Exploration of the Domain of Residue Classes. - Andreas Meier 002; Martin Pollet; Volker Sorge (J. Symb. Comput., 2002)

Interactive Theorem Proving with Tasks. - Malte Hübner; Serge Autexier; Christoph Benzmüller; Andreas Meier 002 (UITP@TPHOLs, 2003)

Adaptable Mixed-Initiative Proof Planning for Educational Interaction. - Andreas Meier 002; Erica Melis; Martin Pollet (UITP@TPHOLs, 2003)

Automatic Generation of Classification Theorems for Finite Algebras. - Simon Colton; Andreas Meier 002; Volker Sorge; Roy L. McCasland (IJCAR, 2004)

Adaptive Access to a Proof Planner. - Erica Melis; Andreas Meier 002; Martin Pollet (MKM, 2004)

Failure Reasoning in Multiple-Strategy Proof Planning. - Andreas Meier 002; Erica Melis (STRATEGIES@IJCAR, 2004)

Bridging Theorem Proving and Mathematical Knowledge Retrieval. - Christoph Benzmüller; Andreas Meier 002; Volker Sorge (Mechanizing Mathematical Reasoning, 2005)

System Description: Multi A Multi-strategy Proof Planner. - Andreas Meier 002; Erica Melis (CADE, 2005)

A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. - Serge Autexier; Christoph Benzmüller; Dominik Dietrich; Andreas Meier 002; Claus-Peter Wirth (MKM, 2005)

Impasse-Driven Reasoning in Proof Planning. - Andreas Meier 002; Erica Melis (MKM, 2005)

A New Set of Algebraic Benchmark Problems for SAT Solvers. - Andreas Meier 002; Volker Sorge (SAT, 2005)

Applying SAT Solving in Classification of Finite Algebras. - Andreas Meier 002; Volker Sorge (J. Autom. Reason., 2005)

Omega. - Christoph Benzmüller; Armin Fiedler; Andreas Meier 002; Martin Pollet; Jörg H. Siekmann (The Seventeen Provers of the World, 2006)

Proof planning with multiple strategies. - Andreas Meier 002 (2007)

Proof planning with multiple strategies. - Erica Melis; Andreas Meier 002; Jörg H. Siekmann (Artif. Intell., 2008)

Automatic Construction and Verification of Isotopy Invariants. - Volker Sorge; Andreas Meier 002; Roy L. McCasland; Simon Colton (J. Autom. Reason., 2008)

Designing a GUI for Proofs - Evaluation of an HCI Experiment - Martin Homik; Andreas Meier 002 (CoRR, 2009)