English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 DetailsSummary
  Semantically Guided First-Order Theorem Proving using Hyper-Linking

Chu, H., & Plaisted, D. A. (1994). Semantically Guided First-Order Theorem Proving using Hyper-Linking. In A. Bundy (Ed.), Proceedings of the 12th International Conference on Automated Deduction (CADE-12) (pp. 192-206). Berlin, Germany: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-ADA0-2 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-ADA1-F
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Chu, Heng, Author
Plaisted, David A.1, Author
Affiliations:
1Max Planck Society, ou_persistent13              

Content

show
hide
Free keywords: -
 Abstract: We present a new procedure, {\em semantic hyper-linking} which uses semantics to guide an instance-based clause-form theorem prover. Semantics for the input clauses is given as input. During the search for the proof, ground instances of the input clauses are generated and new semantic structures are built based on the input semantics and a model of the ground clause set. A proof is found if the ground clause set is unsatisfiable. We give some results in proving hard theorems using semantic hyper-linking; no other special human guidance was given to prove these hard problems. We also show that our method is powerful even with a trivial semantics (that is, even with no guidance in the form of semantic information).

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121994
 Publication Status: Issued
 Pages: -
 Publishing info: Berlin, Germany : Springer
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519496
Other: Local-ID: C1256104005ECAFC-37D96251C514955DC1256144006245EE-chpl:94a
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Nancy, France
Start-/End Date: 1994

Legal Case

show

Project information

show

Source 1

show
hide
Title: Proceedings of the 12th International Conference on Automated Deduction (CADE-12)
Source Genre: Proceedings
 Creator(s):
Bundy, Alan1, Editor           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 192 - 206 Identifier: -

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: - Identifier: -