A Machine-Oriented Logic Based on the Resolution Principle
From MaRDI portal
Publication:5514129
DOI10.1145/321250.321253zbMath0139.12303OpenAlexW2100738443WikidataQ55880673 ScholiaQ55880673MaRDI QIDQ5514129
Publication date: 1965
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321250.321253
Related Items (only showing first 100 items - show all)
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 \(\overline\lambda\)-calculus ⋮ Experimental tests of resolution-based theorem-proving strategies ⋮ An implementation of hyper-resolution ⋮ Analytic resolution in theorem proving ⋮ Mechanizing \(\omega\)-order type theory through unification ⋮ On the complexity of regular resolution and the Davis-Putnam procedure ⋮ A theory of type polymorphism in programming ⋮ Towards the automation of set theory and its logic ⋮ Metamathematical approach to proving theorems of discrete mathematics ⋮ A proof-scheme in discrete mathematics ⋮ Paramodulated connection graphs ⋮ Electronic circuit diagnostic expert systems - a survey ⋮ Recursive query processing: The power of logic ⋮ Complete sets of transformations for general E-unification ⋮ Extending the type checker of Standard ML by polymorphic recursion ⋮ Unification problem in equational theories ⋮ The intractability of resolution ⋮ Properties of substitutions and unifications ⋮ Complete problems in the first-order predicate calculus
This page was built for publication: A Machine-Oriented Logic Based on the Resolution Principle
