Extracting models from clause sets saturated under semantic refinements of the resolution rule.
type: Item
instance of: scholarly article
title: Extracting models from clause sets saturated under semantic refinements of the resolution rule.
zbMATH Open document ID: 1054.68143
DOI: 10.1016/S0890-5401(03)00016-6
author: Nicolas Peltier
published in: Information and Computation
publication date: 2003-08-19T00:00:00Z
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1967122
zbMATH Keywords: Logic in computer science
zbMATH Keywords: Automated deduction
zbMATH Keywords: Automated model building
zbMATH Keywords: Saturation-based methods
describes a project that uses: FINDER
MaRDI profile type: Publication
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: A method for simultaneous search for refutations and models by equational constraint solving
cites work: Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
cites work: Equational problems and disunification
cites work: Q4297316
cites work: Resolution methods for the decision problem
cites work: Decision procedures and model building in equational clause logic
cites work: Hyperresolution and automated model building
cites work: Resolution decision procedures
cites work: Q3996619
cites work: Hyperresolution for guarded formulae
cites work: Q4809060
cites work: Using resolution for testing modal satisfiability and building models
cites work: Resolution Strategies as Decision Procedures
cites work: Explicit representation of terms defined by counter examples
cites work: Q4331764
cites work: Q3142019
cites work: Q4139711
cites work: Representing and building models for decidable subclasses of equational clausal logic
cites work: Pruning the search space and extracting more models in tableaux
cites work: A calculus combining resolution and enumeration for building finite models
cites work: Increasing model building capabilities by constraint solving on terms with integer exponents
cites work: Q4539642
cites work: Q4263159
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Automatic Theorem Proving With Renamable and Semantic Resolution
cites work: Using resolution for deciding solvable classes and building finite models
cites work: An improved lower bound for the elementary theories of trees
description: scientific article; zbMATH DE number 1967122