scientific article; zbMATH DE number 976360
From MaRDI portal
Publication:4331764
zbMath0867.68095MaRDI QIDQ4331764
Publication date: 5 February 1997
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Hypothesis finding based on upward refinement of residue hypotheses. ⋮ Ceres in intuitionistic logic ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Formalization of the resolution calculus for first-order logic ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Towards a clausal analysis of cut-elimination ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Cut-elimination and redundancy-elimination by resolution ⋮ Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria ⋮ Analogy in Automated Deduction: A Survey ⋮ Cut-elimination: syntax and semantics ⋮ Mechanising first-order temporal resolution ⋮ A superposition calculus for abductive reasoning ⋮ Multimodal logic programming ⋮ Towards an algorithmic construction of cut-elimination procedures ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Combining induction and saturation-based theorem proving ⋮ Formalization of the Resolution Calculus for First-Order Logic ⋮ Combining Instance Generation and Resolution ⋮ Completeness of hyper-resolution via the semantics of disjunctive logic programs ⋮ Deciding the \(E^+\)-class by an a posteriori, liftable order ⋮ Controlling witnesses ⋮ Working with ARMs: Complexity results on atomic representations of Herbrand models ⋮ Adding Guarded Constructions to the Syllogistic ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Group cancellation and resolution
