MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance

1. Baumgartner, P., Fuchs, A., Tinelli, C.: Darwin - A Theorem Prover for the Model Evolution Calculus. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning (2004)

   Google Scholar 

2. Carlson, A., Cumby, C., Rosen, J., Roth, D.: SNoW User’s Guide. Technical Report UIUC-DCS-R-99-210, University of Illinois, Urbana-Champaign (1999)

   Google Scholar 

3. Claessen, K., Sorensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)

   Google Scholar 

4. Denney, E., Fischer, B., Schumann, J.: Using Automated Theorem Provers to Certify Auto-generated Aerospace Software. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 198–212. Springer, Heidelberg (2004)

   Google Scholar 

5. Fuchs, M.: Controlled Use of Clausal Lemmas in Connection Tableau Calculi. Journal of Symbolic Computation 29(2), 299–341 (2000)

   Article  MATH  MathSciNet  Google Scholar 

6. McCune, W.W.: Mace4 Reference Manual and Guide. Technical Report ANL/MCS-TM-264, Argonne National Laboratory, Argonne, USA (2003)

   Google Scholar 

7. Meng, J., Paulson, L.: Lightweight Relevance Filtering for Machine-Generated Resolution Problems. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of the FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning. CEUR Workshop Proceedings, vol. 192, pp. 53–69 (2006)

   Google Scholar 

8. Meng, J., Paulson, L.: Translating Higher-order Problems to First-order Clauses. Journal of Automated Reasoning 40(1), 35–60 (2008)

   Article  MATH  MathSciNet  Google Scholar 

9. Plaisted, D.A., Yahya, A.: A Relevance Restriction Strategy for Automated Deduction. Artificial Intelligence 144(1-2), 59–93 (2003)

   Article  MATH  MathSciNet  Google Scholar 

10. Pudlak, P.: Search for Faster and Shorter Proofs using Machine Generated lemmas. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of the FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning. CEUR Workshop Proceedings, vol. 192, pp. 34–52 (2006)

    Google Scholar 

11. Pudlak, P.: Draft Thesis: Verification of Mathematical Proofs (2007)

    Google Scholar 

12. Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers, Dordrecht (1992)

    MATH  Google Scholar 

13. Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: Expressiveness and Efficiency in a Common Sense Knowledge Base. In: Shvaiko, P. (ed.) Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications (2005)

    Google Scholar 

14. Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications 15(2-3), 91–110 (2002)

    MATH  Google Scholar 

15. Schulz, S.: E: A Brainiac Theorem Prover. AI Communications 15(2-3), 111–126 (2002)

    MATH  Google Scholar 

16. Sutcliffe, G.: The 3rd IJCAR Automated Theorem Proving Competition. AI Communications 20(2), 117–126 (2007)

    MathSciNet  Google Scholar 

17. Sutcliffe, G., Dvorsky, A.: Proving Harder Theorems by Axiom Reduction. In: Russell, I., Haller, S. (eds.) Proceedings of the 16th International FLAIRS Conference, pp. 108–112. AAAI Press, Menlo Park (2003)

    Google Scholar 

18. Sutcliffe, G., Puzis, Y.: SRASS - a Semantic Relevance Axiom Selection System. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295–310. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

19. Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)

    Article  MATH  MathSciNet  Google Scholar 

20. Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems. Frontiers in Artificial Intelligence and Applications, vol. 112, pp. 201–215. IOS Press, Amsterdam (2004)

    Google Scholar 

21. Urban, J.: MizarMode - An Integrated Proof Assistance Tool for the Mizar Way of Formalizing Mathematics. Journal of Applied Logic 4(4), 414–427 (2006)

    Article  MATH  MathSciNet  Google Scholar 

22. Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning 37(1-2), 21–43 (2006)

    Article  MATH  Google Scholar 

23. Urban, J.: MaLARea: a Metasystem for Automated Reasoning in Large Theories. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, pp. 45–58 (2007)

    Google Scholar 

24. Veroff, R.: Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies. Journal of Automated Reasoning 16(3), 223–239 (1996)

    Article  MATH  MathSciNet  Google Scholar 

25. Weidenbach, C.: Combining Superposition, Sorts and Splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965–2011. Elsevier Science, Amsterdam (2001)

    Chapter  Google Scholar 

26. Zhang, Y., Sutcliffe, G.: Lemma Management Techniques for Automated Theorem Proving. In: Konev, B., Schulz, S. (eds.) Proceedings of the 5th International Workshop on the Implementation of Logics, pp. 87–94 (2005)

    Google Scholar 

Download references