English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  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/21.11116/0000-000E-081E-9
Genre: Conference Paper

Files

show Files

Locators

show
hide
Locator:
https://rdcu.be/dtofk (Publisher version)
Description:
-
OA-Status:
Not specified

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: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519496
Other: Local-ID: C1256104005ECAFC-37D96251C514955DC1256144006245EE-chpl:94a
DOI: 10.1007/3-540-58156-1_14
BibTex Citekey: Chu/Plaisted_CADE94
 Degree: -

Event

show
hide
Title: 12th International Conference on Automated Deduction
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)
  Abbreviation : CADE 1994
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: ISBN: 978-3-540-58156-7

Source 2

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