MODEL FINDING IN SEMANTICALLY GUIDED INSTANCE-BASED THEOREM PROVING

1 January 1994

journal article
Published by SAGE Publications in Fundamenta Informaticae

Vol. 21 (3) , 221-235
https://doi.org/10.3233/fi-1994-2134

Abstract

Semantic hyper-linking has recently been proposed as a way to use semantics in an instance-based theorem prover. The basic procedure is to use semantics to help generate ground instances of the input clauses until the ground clause set is unsatisfiab

Keywords

MODEL
INSTANCE
SEMANTICS
THEOREM
CLAUSE
UNSATISFIAB
HYPER
INPUT
GUIDED
BASIC

This publication has 0 references indexed in Scilit: