On the modelling of search in theorem proving -- towards a theory of strategy analysis
From MaRDI portal
Publication:1281504
DOI10.1006/inco.1998.2739zbMath0927.68081MaRDI QIDQ1281504
Maria Paola Bonacina, Jieh Hsiang
Publication date: 22 March 1999
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.1998.2739
Related Items
On the modelling of search in theorem proving -- towards a theory of strategy analysis, Towards a unified model of search in theorem-proving: subgoal-reduction strategies
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Towards a foundation of completion procedures as semidecision procedures
- How to avoid the derivation of redundant clauses in reasoning systems
- Theorem-proving with resolution and superposition
- Automated proofs of the Moufang identities in alternative rings
- The intractability of resolution
- Critical pair criteria for completion
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- Lower bounds for increasing complexity of derivations after cut elimination
- SETHEO: A high-performance theorem prover
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- The use of lemmas in the model elimination procedure
- Solution of the Robbins problem
- Proof lengths for equational completion
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- Lower Bounds on Herbrand's Theorem
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- SPASS & FLOTTER version 0.42
- The Complexity of Propositional Proofs
- On fairness of completion-based theorem proving strategies
- The search efficiency of theorem proving strategies
- An application of automated equational reasoning to many-valued logic
- Completion of first-order clauses with equality by strict superposition
- Completion procedures as semidecision procedures
