Elamur Research⌕
☰
home / papers / 2007 / MaLARea: a Metasystem for Automated Reasoning in Large Theories

MaLARea: a Metasystem for Automated Reasoning in Large Theories

Paper · 2007 · Josef Urban

Summary

Resolution-based automated theorem provers (ATPs) tend to struggle when a problem has many irrelevant axioms. This is common in large formal libraries such as Mizar and in knowledge bases like SUMO or CyC. MaLARea addresses this with a small metasystem of about 1000 lines of Perl. It alternates proving attempts by E and SPASS with learning from the proofs that succeed. Learning uses SNoW in naive Bayesian mode. Each formula is characterized only by the symbols it contains. From these symbols, the learner ranks all available axioms by expected relevance, and only the top-ranked ones are passed to the provers in the next round. A greedy control loop starts with few axioms and short time limits. On failure, it first enlarges the axiom budget and then the time budget, and it resets both to the minimum whenever a new proof is found. When evaluated on the MPTP Challenge's chainy problem set, MaLARea solved noticeably more problems than E or SPASS did individually, and it also outperformed the SRASS metasystem. This suggests that reusing knowledge from earlier proofs is a practical way to make ATPs viable in large theories.

Key points

  • The components are E 0.99, SPASS 2.2, SNoW 3.0.3 and the TPTPWorld tools tptp4X and GetSymbols. Vampire was left out because its proof output is hard to parse for the axioms a proof actually used.
  • The benchmark is the MPTP Challenge chainy division: 252 problems in a Mizar-derived theory with 1234 formulas and 418 symbols.
  • MaLARea solved 142 of the 252 problems. For comparison, E solved 89, SPASS 81, and SRASS 126.
  • The control loop uses time limits of 1, 4, 16 and 64 s and axiom limits from 4 up to 128. It stops after at most 1000 iterations.
  • The system assumes that formula names and symbol meanings are consistent across all problem files. It uses no Mizar-specific knowledge, and the author lists richer features, lemmatization and weakening as future work.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Josef Urban. 2007. MaLARea: a Metasystem for Automated Reasoning in Large Theories. ESARLT 2007, CEUR-WS Vol-257.

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{urban2007malarea,
  title = {{MaLARea: a Metasystem for Automated Reasoning in Large Theories}},
  author = {Josef Urban},
  booktitle = {ESARLT 2007, CEUR-WS Vol-257},
  year = {2007},
  url = {http://ceur-ws.org/Vol-257/}
}

References

18 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. A. J. Carlson, C. M. Cumby, J. L. Rosen, and D. Roth. Snow user’s guide. Technical Report UIUC-DCS-R-99-210, UIUC, 1999. find
  2. Koen Claessen and Niklas Sörensson. New techniques that improve MACE-style model finding. In Proc. of Workshop on Model Computation (MODEL), 2003. find
  3. J. Denzinger, M. Fuchs, C. Goller, and S. Schulz. Learning from Previous Proof Experience. Technical Report AR99-4, Institut für Informatik, Technische Universität München, 1999. (also to be published as a SEKI report). find
  4. C. Matuszek, Cabral J., M. Witbrock, and J. DeOliveira. An Introduction to the Syntax and Content of Cyc. In Baral C., editor, Proceedings of the 2006 AAAI Spring Symposium on Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering, page… find
  5. Jia Meng and L. C. Paulson. Lightweight relevance filtering for machine-generated resolution problems. In Geoff Sutcliffe, Renate Schmidt, and Stephan Schulz, editors, ESCoR: Empirically Successful Computerized Reasoning, volume 192 of CEUR Workshop Proceedings, pages 53–69. CEUR, 2006. find
  6. Jia Meng and L. C. Paulson. Translating higher-order problems to first-order clauses. In Geoff Sutcliffe, Renate Schmidt, and Stephan Schulz, editors, ESCoR: Empirically Successful Computerized Reasoning, volume 192 of CEUR Workshop Proceedings, pages 70–80. CEUR, 2006. find
  7. Ian Niles and Adam Pease. Towards a standard upper ontology. In FOIS ’01: Proceedings of the international conference on Formal Ontology in Information Systems, pages 2–9, New York, NY, USA, 2001. ACM Press. find
  8. Monty Newborn and Zongyan Wang. Octopus: Combining learning and parallel search. J. Autom. Reasoning, 33(2):171–218, 2004. find
  9. Petr Pudlák. Search for faster and shorter proofs using machine generated lemmas. In Geoff Sutcliffe, Renate Schmidt, and Stephan Schulz, editors, ESCoR: Empirically Successful Computerized Reasoning, volume 192 of CEUR Workshop Proceedings, pages 34–52. CEUR, 2006. find
  10. Alexandre Riazanov and Andrei Voronkov. The design and implementation of VAMPIRE. Journal of AI Communications, 15(2-3):91–110, 2002. find
  11. S. Schulz. E – a brainiac theorem prover. Journal of AI Communications, 15(2-3):111–126, 2002. find
  12. G. Sutcliffe and C.B. Suttner. The TPTP problem library: CNF release v1.2.1. Journal of Automated Reasoning, 21(2):177–203, 1998. find
  13. G. Sutcliffe. The Design and Implementation of a Compositional Competition-Cooperation Parallel ATP System. In H. de Nivelle and S. Schulz, editors, Proceedings of the 2nd International Workshop on the Implementation of Logics, number MPI-I-2001-2-006 in Max-Planck-Institut für Informatik, Research… find
  14. G. Sutcliffe and Puzis Y. SRASS - a semantic relevance axiom selection system. In Pfenning F., editor, CADE 2007, Lecture Notes in Artificial Intelligence. Springer, 2007. To appear. find
  15. G. Sutcliffe, J. Zimmer, and S. Schulz. TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In V. Sorge and W. Zhang, editors, Distributed and Multi-Agent Reasoning, Frontiers in Artificial Intelligence and Applications. IOS Press, 2004. find
  16. Josef Urban. MPTP - motivation, implementation, first experiments. Journal of Automated Reasoning, 33(3-4):319–339, 2004. find
  17. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  18. C. Weidenbach. Handbook of Automated Reasoning, volume II, chapter SPASS: Combining Superposition, Sorts and Splitting, pages 1965–2013. Elsevier and MIT Press, 2001. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/urban-2007-malarea-metasystem-automated-reasoning-large/