On the modelling of search in theorem proving -- towards a theory of strategy analysis
type: Item
instance of: scholarly article
title: On the modelling of search in theorem proving -- towards a theory of strategy analysis
zbMATH Open document ID: 0927.68081
author: Jieh Hsiang
author: Maria Paola Bonacina
published in: Information and Computation
publication date: 1999-03-22T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1267929
zbMATH Keywords: theorem proving
zbMATH Keywords: contraction
describes a project that uses: SETHEO
describes a project that uses: OTTER
describes a project that uses: EQP
describes a project that uses: SPASS
describes a project that uses: METEOR
describes a project that uses: RRL
describes a project that uses: FLOTTER
MaRDI profile type: Publication
full work available at URL: inco.1998.2739
OpenAlex ID: W2063169961
cites work: An application of automated equational reasoning to many-valued logic
cites work: Automated proofs of the Moufang identities in alternative rings
cites work: The use of lemmas in the model elimination procedure
cites work: Critical pair criteria for completion
cites work: Q3427354
cites work: Completion of first-order clauses with equality by strict superposition
cites work: Q4255513
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Completion procedures as semidecision procedures
cites work: On fairness of completion-based theorem proving strategies
cites work: Towards a foundation of completion procedures as semidecision procedures
cites work: Q5679729
cites work: The relative efficiency of propositional proof systems
cites work: Q4385532
cites work: Q3997615
cites work: Q4942635
cites work: The intractability of resolution
cites work: Q3028369
cites work: Q5623241
cites work: SETHEO: A high-performance theorem prover
cites work: Q4229404
cites work: Solution of the Robbins problem
cites work: Lower bounds for increasing complexity of derivations after cut elimination
cites work: The search efficiency of theorem proving strategies
cites work: Proof lengths for equational completion
cites work: Theorem-proving with resolution and superposition
cites work: How to avoid the derivation of redundant clauses in reasoning systems
cites work: Lower Bounds on Herbrand's Theorem
cites work: A Prolog technology theorem prover: Implementation by an extended Prolog compiler
cites work: Hard examples for resolution
cites work: The Complexity of Propositional Proofs
cites work: SPASS & FLOTTER version 0.42
cites work: On restrictions of ordered paramodulation with simplification
DOI: 10.1006/INCO.1998.2739
description: scientific article; zbMATH DE number 1267929