---
title: "MaLARea — paper by Urban (2007) — summary and ideas"
description: "Resolution-based automated theorem provers (ATPs) tend to struggle when a problem has many… 18 references, cited by 6 papers here."
authors: ["Josef Urban"]
year: 2007
venue: "ESARLT 2007, CEUR-WS Vol-257"
source: "http://ceur-ws.org/Vol-257/"
licence: "All rights reserved — free to read at the source"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/urban-2007-malarea-metasystem-automated-reasoning-large/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/urban-2007-malarea-metasystem-automated-reasoning-large/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2007](https://md.research.elamur.ai/free/en/papers/2007/) / MaLARea: a Metasystem for Automated Reasoning in Large Theories

# MaLARea: a Metasystem for Automated Reasoning in Large Theories

**Authors:** [Josef Urban](https://md.research.elamur.ai/free/en/authors/josef-urban/) · **Year:** 2007 · **Venue:** ESARLT 2007, CEUR-WS Vol-257 · **Licence:** All rights reserved — free to read at the source

**Links:** [Publisher's page](http://ceur-ws.org/Vol-257/) · [PDF](http://ceur-ws.org/Vol-257/05_Urban.pdf) · [OpenAlex](https://openalex.org/W1500667683)

**Citations:** 46 citations (OpenAlex, 2026-10-14) · [6](https://md.research.elamur.ai/free/en/papers/urban-2007-malarea-metasystem-automated-reasoning-large/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## 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.*

📚 Shelves (2): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/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.

```bibtex
@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/}
}
```

- [← previous SemEval-2007 Task 19: Frame Semantic Structure Extraction](https://md.research.elamur.ai/free/en/papers/baker-2007-semeval-2007-task-19-frame/)
- [next → Multiple Sluicing in English](https://md.research.elamur.ai/free/en/papers/park-2007-multiple-sluicing-english/)
- [↑ back to papers of 2007](https://md.research.elamur.ai/free/en/papers/2007/)

## 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](https://scholar.google.com/scholar?q=A%2E+J%2E+Carlson%2C+C%2E+M%2E+Cumby%2C+J%2E+L%2E+Rosen%2C+and+D%2E+Roth%2E+Snow+user%E2%80%99s+guide%2E+Technical+Report+UIUC%2DDCS%2DR%2D99%2D210%2C+UIUC%2C+1999%2E)
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](https://scholar.google.com/scholar?q=Koen+Claessen+and+Niklas+So%CC%88rensson%2E+New+techniques+that+improve+MACE%2Dstyle+model+finding%2E+In+Proc%2E+of+Workshop+on+Model+Computation+%28MODEL%29%2C+2003%2E)
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](https://scholar.google.com/scholar?q=J%2E+Denzinger%2C+M%2E+Fuchs%2C+C%2E+Goller%2C+and+S%2E+Schulz%2E+Learning+from+Previous+Proof+Experience%2E+Technical+Report+AR99%2D4%2C+Institut+fu%CC%88r+Informatik%2C+Technische+Universita%CC%88t+Mu%CC%88nchen%2C+1999%2E+%28also+to+be+publis)
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](https://scholar.google.com/scholar?q=C%2E+Matuszek%2C+Cabral+J%2E%2C+M%2E+Witbrock%2C+and+J%2E+DeOliveira%2E+An+Introduction+to+the+Syntax+and+Content+of+Cyc%2E+In+Baral+C%2E%2C+editor%2C+Proceedings+of+the+2006+AAAI+Spring+Symposium+on+Formalizing+and+Compilin)
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](https://scholar.google.com/scholar?q=Jia+Meng+and+L%2E+C%2E+Paulson%2E+Lightweight+relevance+filtering+for+machine%2Dgenerated+resolution+problems%2E+In+Geoff+Sutcliffe%2C+Renate+Schmidt%2C+and+Stephan+Schulz%2C+editors%2C+ESCoR%3A+Empirically+Successful+Co)
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](https://scholar.google.com/scholar?q=Jia+Meng+and+L%2E+C%2E+Paulson%2E+Translating+higher%2Dorder+problems+to+first%2Dorder+clauses%2E+In+Geoff+Sutcliffe%2C+Renate+Schmidt%2C+and+Stephan+Schulz%2C+editors%2C+ESCoR%3A+Empirically+Successful+Computerized+Reason)
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](https://scholar.google.com/scholar?q=Ian+Niles+and+Adam+Pease%2E+Towards+a+standard+upper+ontology%2E+In+FOIS+%E2%80%9901%3A+Proceedings+of+the+international+conference+on+Formal+Ontology+in+Information+Systems%2C+pages+2%E2%80%939%2C+New+York%2C+NY%2C+USA%2C+2001%2E+ACM)
8. Monty Newborn and Zongyan Wang. Octopus: Combining learning and parallel search. J. Autom. Reasoning, 33(2):171–218, 2004. [find](https://scholar.google.com/scholar?q=Monty+Newborn+and+Zongyan+Wang%2E+Octopus%3A+Combining+learning+and+parallel+search%2E+J%2E+Autom%2E+Reasoning%2C+33%282%29%3A171%E2%80%93218%2C+2004%2E)
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](https://scholar.google.com/scholar?q=Petr+Pudla%CC%81k%2E+Search+for+faster+and+shorter+proofs+using+machine+generated+lemmas%2E+In+Geoff+Sutcliffe%2C+Renate+Schmidt%2C+and+Stephan+Schulz%2C+editors%2C+ESCoR%3A+Empirically+Successful+Computerized+Reasoning)
10. Alexandre Riazanov and Andrei Voronkov. The design and implementation of VAMPIRE. Journal of AI Communications, 15(2-3):91–110, 2002. [find](https://scholar.google.com/scholar?q=Alexandre+Riazanov+and+Andrei+Voronkov%2E+The+design+and+implementation+of+VAMPIRE%2E+Journal+of+AI+Communications%2C+15%282%2D3%29%3A91%E2%80%93110%2C+2002%2E)
11. S. Schulz. E – a brainiac theorem prover. Journal of AI Communications, 15(2-3):111–126, 2002. [find](https://scholar.google.com/scholar?q=S%2E+Schulz%2E+E+%E2%80%93+a+brainiac+theorem+prover%2E+Journal+of+AI+Communications%2C+15%282%2D3%29%3A111%E2%80%93126%2C+2002%2E)
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](https://scholar.google.com/scholar?q=G%2E+Sutcliffe+and+C%2EB%2E+Suttner%2E+The+TPTP+problem+library%3A+CNF+release+v1%2E2%2E1%2E+Journal+of+Automated+Reasoning%2C+21%282%29%3A177%E2%80%93203%2C+1998%2E)
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](https://scholar.google.com/scholar?q=G%2E+Sutcliffe%2E+The+Design+and+Implementation+of+a+Compositional+Competition%2DCooperation+Parallel+ATP+System%2E+In+H%2E+de+Nivelle+and+S%2E+Schulz%2C+editors%2C+Proceedings+of+the+2nd+International+Workshop+on+th)
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](https://scholar.google.com/scholar?q=G%2E+Sutcliffe+and+Puzis+Y%2E+SRASS+%2D+a+semantic+relevance+axiom+selection+system%2E+In+Pfenning+F%2E%2C+editor%2C+CADE+2007%2C+Lecture+Notes+in+Artificial+Intelligence%2E+Springer%2C+2007%2E+To+appear%2E)
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](https://scholar.google.com/scholar?q=G%2E+Sutcliffe%2C+J%2E+Zimmer%2C+and+S%2E+Schulz%2E+TSTP+Data%2DExchange+Formats+for+Automated+Theorem+Proving+Tools%2E+In+V%2E+Sorge+and+W%2E+Zhang%2C+editors%2C+Distributed+and+Multi%2DAgent+Reasoning%2C+Frontiers+in+Artificia)
16. Josef Urban. MPTP - motivation, implementation, first experiments. Journal of Automated Reasoning, 33(3-4):319–339, 2004. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+MPTP+%2D+motivation%2C+implementation%2C+first+experiments%2E+Journal+of+Automated+Reasoning%2C+33%283%2D4%29%3A319%E2%80%93339%2C+2004%2E)
17. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+MPTP+0%2E2%3A+Design%2C+implementation%2C+and+initial+experiments%2E+J%2E+Autom%2E+Reasoning%2C+37%281%2D2%29%3A21%E2%80%9343%2C+2006%2E)
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](https://scholar.google.com/scholar?q=C%2E+Weidenbach%2E+Handbook+of+Automated+Reasoning%2C+volume+II%2C+chapter+SPASS%3A+Combining+Superposition%2C+Sorts+and+Splitting%2C+pages+1965%E2%80%932013%2E+Elsevier+and+MIT+Press%2C+2001%2E)

*Updated 3 November 2026*