Extracting models from clause sets saturated under semantic refinements of the resolution rule.

DOI10.1016/S0890-5401(03)00016-6zbMath1054.68143MaRDI QIDQ1401929

Nicolas Peltier

Publication date: 19 August 2003

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

Automated deductionAutomated model buildingLogic in computer scienceSaturation-based methods

Mathematics Subject Classification ID

Uses Software

• FINDER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Representing and building models for decidable subclasses of equational clausal logic
• Explicit representation of terms defined by counter examples
• Equational problems and disunification
• A method for simultaneous search for refutations and models by equational constraint solving
• Resolution methods for the decision problem
• Increasing model building capabilities by constraint solving on terms with integer exponents
• A calculus combining resolution and enumeration for building finite models
• Hyperresolution for guarded formulae
• Using resolution for testing modal satisfiability and building models
• Resolution Strategies as Decision Procedures
• Pruning the search space and extracting more models in tableaux
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Decision procedures and model building in equational clause logic
• Using resolution for deciding solvable classes and building finite models
• An improved lower bound for the elementary theories of trees
• Hyperresolution and automated model building
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Combining enumeration and deductive techniques in order to increase the class of constructible infinite models

This page was built for publication: Extracting models from clause sets saturated under semantic refinements of the resolution rule.