Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures

DOI10.1007/BF00885766zbMath0805.68103OpenAlexW1994344807MaRDI QIDQ1340966

Chih-Hung Wu, Shie-Jue Lee

Publication date: 21 December 1994

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00885766

zbMATH Keywords

theorem provingfirst-order logicunificationclause networkhyperlinks

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Uses Software

• TPTP
• CLIPS
• CLIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Eliminating dublication with the hyper-linking strategy
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• A structure-preserving clause form translation
• Seventy-five problems for testing automatic theorem provers
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• A simplified problem reduction format
• Complexity and related enhancements for automated theorem-proving programs
• Non-resolution theorem proving
• The TPTP problem library. CNF release v1. 2. 1
• Problem solving by searching for models with a theorem prover
• Problem corner: Non-Horn problems
• Theorem-Proving on the Computer
• Synthesizing constraint expressions
• A Computing Procedure for Quantification Theory

This page was built for publication: Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures