A Machine-Oriented Logic Based on the Resolution Principle

Cited in

(only showing first 100 items - show all)

Lightweight relevance filtering for machine-generated resolution problems
A combinatorial characterization of treelike resolution space
An approach for extracting a small unsatisfiable core
A new methodology for developing deduction methods
First order Stålmarck. Universal lemmas through branch merges
Completeness of hyper-resolution via the semantics of disjunctive logic programs
A simple deduction method for modal logic
Fundamental properties of infinite trees
Automated theorem proving methods
On the correspondence between two classes of reduction systems
Condensed detachment as a rule of inference
A superposition oriented theorem prover
A mechanical solution of Schubert's steamroller by many-sorted resolution
Rewrite systems on a lattice of types
Equational methods in first order predicate calculus
The intractability of resolution
Properties of substitutions and unifications
Complete problems in the first-order predicate calculus
The occur-check problem in Prolog
Inserting injection operations to denotational specifications
A parallel algorithm for the monadic unification problem
On solving the equality problem in theories defined by Horn clauses
An algebraic semantics approach to the effective resolution of type equations
A refinement of strong sequentiality for term rewriting with constructors
The implementation of FPROLOG - a fuzzy PROLOG interpreter
Resolution on formula-trees
Associative-commutative unification
Unification in combinations of collapse-free regular theories
An algebraic approach to unification under associativity and commutativity
Resolution vs. cutting plane solution of inference problems: Some computational experience
Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
Inconsistency check of a set of clauses using Petri net reductions
Some results and experiments in programming techniques for propositional logic
Embedding Boolean expressions into logic programming
On conceptual model specification and verification
A class of confluent term rewriting systems and unification
A parallel approach for theorem proving in propositional logic
History and basic features of the critical-pair/completion procedure
About the Paterson-Wegman linear unification algorithm
The recursive resolution method for modal logic
A practically efficient and almost linear unification algorithm
A unification algorithm for second-order monadic terms
Principal type scheme and unification for intersection type discipline
Polymorphic type inference and containment
Generalized subsumption and its applications to induction and redundancy
Implication of clauses is undecidable
Unification in Boolean rings
Linear strategy for propositional modal resolution
One modification of the ordering strategy in the resolution method
Fundamentals of Fuzzy Prolog
MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
Inheritance hierarchies: Semantics and unifications
On the relationship of congruence closure and unification
Equational problems and disunification
Equational unification, word unification, and 2nd-order equational unification
Logic applied to integer programming and integer programming applied to logic
Using rewriting rules for connection graphs to prove theorems
A logic for default reasoning
Non-monotonic logic. I
Definite clause grammars for language analysis - A survey of the formalism and a comparison with augmented transition networks
The undecidability of the second-order unification problem
Completely non-clausal theorem proving
An extension to linear resolution with selection function
Lower bounds for increasing complexity of derivations after cut elimination
A simplified problem reduction format
Unifiability is complete for co-N Log Space
Mechanical proof systems for logic: Reaching consensus by groups of intelligent agents
Unfold/fold transformation of stratified programs
Horn clause programs with polymorphic types: Semantics and resolution
Resolution for some first-order modal systems
Completion for unification
Condensed detachment is complete for relevance logic: A computer-aided proof
Implementing the `Fool's model' of combinatory logic
The unification hierarchy is undecidable
Domains for logic programming
Contraction algebras and unification of (infinite) terms
An operational formal definition of PROLOG: A specification method and its application
Reduction rules for resolution-based systems
Discriminator varieties and symbolic computation
A semantic backward chaining proof system
An order-sorted logic for knowledge representation systems
Tseitin's formulas revisited
Complexity of resolution proofs and function introduction
A logic approach to the resolution of constraints in timetabling
The problem of reasoning from inequalities
Gazing: An approach to the problem of definition and lemma use
A new subsumption method in the connection graph proof procedure
Linear resolution for consequence finding
Conceptual graphs as a universal knowledge representation
On the synthesis of function inverses
C-expressions: A variable-free calculus for equational logic programming
My collaboration with Julia Robinson
Reasoning about programs
Knowledge and reasoning in program synthesis
\(\Pi\)-representation: A clause representation for parallel search
On the role of unification in mechanical theorem proving
Refutation graphs
A unification algorithm for typed \(\bar\lambda\)-calculus
Complexity of the unification algorithm for first-order expressions
A unification algorithm for typed -calculus

This page was built for publication: A Machine-Oriented Logic Based on the Resolution Principle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5514129)