The search efficiency of theorem proving strategies
From MaRDI portal
Publication:5210762
Recommendations
- scientific article; zbMATH DE number 1113998
- scientific article; zbMATH DE number 1037485
- Eliminating dublication with the hyper-linking strategy
- 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
Cites work
- A Computing Procedure for Quantification Theory
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A simplified problem reduction format
- Automatic Theorem Proving With Renamable and Semantic Resolution
- Depth-first iterative-deepening: An optimal admissible tree search
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Eliminating dublication with the hyper-linking strategy
- Hard examples for resolution
- scientific article; zbMATH DE number 3860434 (Why is no real title available?)
- scientific article; zbMATH DE number 4200168 (Why is no real title available?)
- scientific article; zbMATH DE number 4104410 (Why is no real title available?)
- scientific article; zbMATH DE number 43398 (Why is no real title available?)
- scientific article; zbMATH DE number 48763 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 194631 (Why is no real title available?)
- scientific article; zbMATH DE number 3254919 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- Non-Horn clause logic programming without contrapositives
- On a bound for the complexity of terms in the resolution method
- On restrictions of ordered paramodulation with simplification
- Proving refutational completeness of theorem-proving strategies
- The intractability of resolution
- The relative efficiency of propositional proof systems
- Using resolution for deciding solvable classes and building finite models
Cited in
(39)- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- Non-Horn clause logic programming
- Limited resource strategy in resolution theorem proving
- Eliminating redundant search space on backtracking for forward chaining theorem proving
- Ordered semantic hyper-linking
- Evaluating general purpose automated theorem proving systems
- On different proof-search strategies for orthologic
- Set of support, demodulation, paramodulation: a historical perspective
- Bayesian ranking for strategy scheduling in automated theorem provers
- Contradiction separation based dynamic multi-clause synergized automated deduction
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Partition-based logical reasoning for first-order and propositional theories
- Theorem proving with structured theories. (Preliminary report)
- Performance of clause selection heuristics for saturation-based theorem proving
- scientific article; zbMATH DE number 2084332 (Why is no real title available?)
- Extension rule algorithms based on IMOM and IBOHM heuristics strategies
- scientific article; zbMATH DE number 3870636 (Why is no real title available?)
- scientific article; zbMATH DE number 3874657 (Why is no real title available?)
- scientific article; zbMATH DE number 3986666 (Why is no real title available?)
- scientific article; zbMATH DE number 1037485 (Why is no real title available?)
- scientific article; zbMATH DE number 1113998 (Why is no real title available?)
- scientific article; zbMATH DE number 1980923 (Why is no real title available?)
- scientific article; zbMATH DE number 2079834 (Why is no real title available?)
- Situational calculus, linear connection proofs and STRIPS-like planning: an experimental comparison
- The design of the CADE-13 ATP system competition
- scientific article; zbMATH DE number 1929148 (Why is no real title available?)
- scientific article; zbMATH DE number 834572 (Why is no real title available?)
- scientific article; zbMATH DE number 1418280 (Why is no real title available?)
- scientific article; zbMATH DE number 1439761 (Why is no real title available?)
- Automated Reasoning with Analytic Tableaux and Related Methods
- Refinements to depth-first iterative-deepening search in automatic theorem proving
- An exhaustive matching procedure for the improvement of learning efficiency.
- Finding shortest proofs: An application of linked inference rules
- A complete semantic back chaining proof system
- Complete inference via knowledge Petri nets and resolution rules
- Eliminating dublication with the hyper-linking strategy
- Considerations on approaches and metrics in automated theorem generation/finding in geometry
- A relevance restriction strategy for automated deduction
This page was built for publication: The search efficiency of theorem proving strategies
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5210762)
