A semantically guided first-order theorem prover CLIN-S. CLIN-S is an instance-based, clause-form first-order theorem prover. CLIN-S employs three inference procedures: semantic hyper-linking, which uses semantics to guide the proof search and performs well on non-Horn parts of the proofs involving small literals, rough resolution, which removes large literals in the proofs, and UR resolution, which proves the Horn parts of the proofs. A semantic structure 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 describe the system architecture and major inference rules used in CLIN-S.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
- Ma, Jun; Li, Wenjiang; Ruan, Da; Xu, Yang: Filter-based resolution principle for lattice-valued propositional logic LP$(X)$ (2007)
- Chu, Heng; Plaisted, David A.: A semantically guided first-order theorem prover CLIN-S. (1997) ioport
- Lee, Shie-Jue; Wu, Chih-Hung: Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures (1994)