Representing and building models for decidable subclasses of equational clausal logic (Q861367): Difference between revisions

@@ Property / DOI @@
-.1007/s10817-004-5555-7
@@ Property / DOI: 10.1007/s10817-004-5555-7 / rank @@
-Normal rank
@@ Property / author @@
-Nicolas Peltier
@@ Property / author: Nicolas Peltier / rank @@
-Normal rank
@@ Property / author @@
+Nicolas Peltier
@@ Property / author: Nicolas Peltier / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SATCHMO
@@ Property / describes a project that uses: SATCHMO / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPASS
@@ Property / describes a project that uses: SPASS / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-004-5555-7
+Normal rank
@@ Property / OpenAlex ID @@
+W1968211553
@@ Property / OpenAlex ID: W1968211553 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751360
@@ Property / cites work: Q2751360 / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Hyper Tableaux with Equality
@@ Property / cites work: Hyper Tableaux with Equality / rank @@
+Normal rank
@@ Property / cites work @@
+Positive unit hyperresolution tableaux and their application to minimal model generation
+Normal rank
@@ Property / cites work @@
+Complete axiomatizations of some quotient term algebras
+Normal rank
@@ Property / cites work @@
+Equational formulae with membership constraints
@@ Property / cites work: Equational formulae with membership constraints / rank @@
+Normal rank
@@ Property / cites work @@
+On the duality of abduction and model generation in a framework for model generation with equality
+Normal rank
@@ Property / cites work @@
+Q3905252
@@ Property / cites work: Q3905252 / rank @@
+Normal rank
@@ Property / cites work @@
+Hyperresolution and automated model building
@@ Property / cites work: Hyperresolution and automated model building / rank @@
+Normal rank
@@ Property / cites work @@
+Decision procedures and model building in equational clause logic
+Normal rank
@@ Property / cites work @@
+Resolution methods for the decision problem
@@ Property / cites work: Resolution methods for the decision problem / rank @@
+Normal rank
@@ Property / cites work @@
+Q2767012
@@ Property / cites work: Q2767012 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751377
@@ Property / cites work: Q2751377 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3996619
@@ Property / cites work: Q3996619 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809060
@@ Property / cites work: Q4809060 / rank @@
+Normal rank
@@ Property / cites work @@
+Hyperresolution for guarded formulae
@@ Property / cites work: Hyperresolution for guarded formulae / rank @@
+Normal rank
@@ Property / cites work @@
+Proving refutational completeness of theorem-proving strategies
+Normal rank
@@ Property / cites work @@
+Q4263163
@@ Property / cites work: Q4263163 / rank @@
+Normal rank
@@ Property / cites work @@
+Using resolution for testing modal satisfiability and building models
+Normal rank
@@ Property / cites work @@
+Resolution Strategies as Decision Procedures
@@ Property / cites work: Resolution Strategies as Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Q5581665
@@ Property / cites work: Q5581665 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3142019
@@ Property / cites work: Q3142019 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4331764
@@ Property / cites work: Q4331764 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4139711
@@ Property / cites work: Q4139711 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3821629
@@ Property / cites work: Q3821629 / rank @@
+Normal rank
@@ Property / cites work @@
+An Efficient Unification Algorithm
@@ Property / cites work: An Efficient Unification Algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+On the decidability of the PVD class with equality
+Normal rank
@@ Property / cites work @@
+A calculus combining resolution and enumeration for building finite models
+Normal rank
@@ Property / cites work @@
+Q4430633
@@ Property / cites work: Q4430633 / rank @@
+Normal rank
@@ Property / cites work @@
+Model building with ordered resolution: Extracting models from saturated clause sets
+Normal rank
@@ Property / cites work @@
+A Resolution-based Model Building Algorithm for a Fragment of OCC1N =
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+SHR Tableaux -- A Framework for Automated Model Generation
+Normal rank
@@ Property / cites work @@
+Automatic Theorem Proving With Renamable and Semantic Resolution
+Normal rank
@@ Property / DOI @@
+.1007/S10817-004-5555-7
@@ Property / DOI: 10.1007/S10817-004-5555-7 / rank @@
+Normal rank