Analysis of theorem-proving strategies
Strategy analysis aims at complementing the experimental
evaluation of theorem provers with mathematical
models of the behavior of strategies that capture
their essential features and establish comparative results.
I developed a methodology for strategy analysis which
models together search space and search process by means of
marked search graphs, and measures search complexity,
even in infinite search spaces,
by means of bounded search spaces.
This also led me to a taxonomy of theorem-proving
strategies based on search rather than inferences:
- Maria Paola Bonacina.
Towards a unified model of search in theorem proving: subgoal-reduction strategies.
Journal of Symbolic Computation, 39(2):209-255, February 2005;
DOI: 10.1016/j.jsc.2004.11.001. (An earlier version was presented at the Dagstuhl Seminar 01101 on Deduction, March 2001)
- Maria Paola Bonacina.
A model and a first analysis of distributed-search contraction-based strategies.
Annals of Mathematics and Artificial Intelligence, 27(1-4):149-199, December 1999;
DOI: 10.1023/A:1018919214722.
- Maria Paola Bonacina.
A taxonomy of theorem proving strategies.
In Artificial Intelligence Today - Recent Trends and Developments,
Springer,
Lecture Notes in Artificial Intelligence 1600, 43-84, August 1999 (invited);
DOI: 10.1007/3-540-48317-9_3.
- Maria Paola Bonacina and Jieh Hsiang.
On the modelling of search in theorem proving - Towards a theory of strategy analysis.
Information and Computation, 147:171-208, December 1998;
DOI: 10.1006/inco.1998.2739.
- Maria Paola Bonacina.
Theorem proving strategies: a search-oriented taxonomy.
In Proceedings of the 2nd International Workshop on First-order Theorem Proving (FTP 1998),
Schloss Wilhelminenberg, Vienna, Austria,
Techical Report E1852-GS-981, Technische Universität Wien, 256-259,
November 1998.
- Maria Paola Bonacina.
Analysis of distributed-search contraction-based strategies.
Proceedings of the 6th Joint European Workshop on Logics in Artificial Intelligence (JELIA),
Springer,
Lecture Notes in Artificial Intelligence 1489, 107-121, October 1998;
DOI: 10.1007/3-540-49545-2_8.
- Maria Paola Bonacina.
Strategy analysis: from sequential to parallel strategies.
In Proceedings of the 2nd Workshop on Strategies in Automated Deduction
(STRATEGIES 1998), CADE-15, 19-21, Lindau, Germany, July 1998.
- Maria Paola Bonacina.
On the representation of parallel search in theorem proving.
In Proceedings of the 1st International Workshop on First-order Theorem Proving (FTP 1997), Schloss Hagenberg, Linz, Austria, October 1997.
Technical Report 97-50, RISC, Johannes Kepler Universität, Linz, 22-28, 1997.
- Maria Paola Bonacina.
Machine-independent evaluation of theorem-proving strategies.
In Proceedings of the 1st Workshop on Strategies in Automated Deduction
(STRATEGIES 1997),
CADE-14, 37-39, Townsville, Queensland, Australia, July 1997.
- Maria Paola Bonacina and Jieh Hsiang.
On the notion of complexity of search in theorem proving.
Logic Colloquium 1996, San Sebastiàn, Spain, July 1996.
Bulletin of Symbolic Logic, 3(2):253-254, June 1997.
- Maria Paola Bonacina.
A note on the analysis of theorem-proving strategies.
Newsletter of the Association for Automated Reasoning, 36:2-8, April 1997.
- Maria Paola Bonacina and Jieh Hsiang.
On the representation of dynamic search spaces in theorem proving.
In Proceedings of the International Conference on Artificial Intelligence,
International Computer Symposium, 85-94, National Sun-Yat Sen University,
Kaohshiung, Taiwan, ROC, December 1996.
- Maria Paola Bonacina.
A note on the analysis of theorem-proving strategies.
Technical Report, Department of Computer Science, The University of Iowa, May 1996, 1-12.
- Maria Paola Bonacina.
Future directions of automated deduction: Strategy analysis for theorem proving.
National Science Foundation Workshop on the Future Directions of Automated Deduction, Chicago, Illinois, USA, April 1996.
A forerunner of this research was a formalization of concepts in theorem proving, including search plan:
Maria Paola Bonacina