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
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, An improved upper bound for SAT, Contract-based verification of MATLAB-style matrix programs, Evidence algorithm and inference search in first-order logics, Unification for infinite sets of equations between finite terms, Semi-intelligible Isar proofs from machine-generated proofs, Quantifier simplification by unification in SMT, Proof complexity of modal resolution, Interprocedural and flow-sensitive type analysis for memory and type safety of C code, Correia semantics revisited, The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem, Optimal length resolution refutations of difference constraint systems, Termination of floating-point computations, Representing and building models for decidable subclasses of equational clausal logic, Some techniques for proving termination of the hyperresolution calculus, Computer supported mathematics with \(\Omega\)MEGA, Invariant-free clausal temporal resolution, Filter-based resolution principle for lattice-valued propositional logic LP\((X)\), The disconnection tableau calculus, Defining answer classes using resolution refutation, Dual erotetic calculi and the minimal \(\mathsf{LFI}\), Learning from conflicts in propositional satisfiability, Extracting the resolution algorithm from a completeness proof for the propositional calculus, On deciding satisfiability by theorem proving with speculative inferences, Dealing with satisfiability and \(n\)-ary CSPs in a logical framework, Structure sharing for quantified terms: Fundamentals, Resolution principles in possibilistic logic, Replacing unification by constraint satisfaction to improve logic program expressiveness, Completeness of resolution revisited, An incremental method for generating prime implicants/implicates, An epistemic model of logic programming, Best unifiers in transitive modal logics, Algorithms for generating arguments and counterarguments in propositional logic, Linearity and iterator types for Gödel's system \(\mathcal T\), Meta-resolution: An algorithmic formalisation, Lazy narrowing: strong completeness and eager variable elimination, Resolution search, Estimating the number of steps that it takes to solve some problems of pattern recognition which admit logical description, An introduction to mechanized reasoning, Enhancing unsatisfiable cores for LTL with information on temporal relevance, Prominent classes of the most general subsumptive solutions of Boolean equations, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, Average-case analysis of unification algorithms, An essay on resolution logics, Parsing as non-Horn deduction, Cut formulas in propositional logic, An approach to completing variable names for implicitly typed functional languages, A calculus for automatic verification of Petri nets based on resolution and dynamic logics, Programming with narrowing: a tutorial, John McCarthy's legacy, On the power of clause-learning SAT solvers as resolution engines, Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\), Resolution is cut-free, The correctness of Newman's typability algorithm and some of its extensions, Enhancing global SLS-resolution with loop cutting and tabling mechanisms, A sound and complete model-generation procedure for consistent and confidentiality-preserving databases, Computer theorem proving in mathematics, On the complexity of cutting-plane proofs, An experimental logic based on the fundamental deduction principle, Unification in Boolean rings and Abelian groups, An almost linear Robinson unification algorithm, Order-sorted unification, Unification in a combination of arbitrary disjoint equational theories, On the parameterized complexity of associative and commutative unification, Lightweight relevance filtering for machine-generated resolution problems, Regular expression order-sorted unification and matching, Automation methods for logical derivation and their application in the control of dynamic and intelligent systems, Clausal presentation of theories in deduction modulo, Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics, A combinatorial characterization of treelike resolution space, A practical unification algorithm, Using forcing to prove completeness of resolution and paramodulation, Theorem-proving with resolution and superposition, A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains, An approach for extracting a small unsatisfiable core, A new methodology for developing deduction methods, First order Stålmarck. Universal lemmas through branch merges, \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic, Completeness of hyper-resolution via the semantics of disjunctive logic programs, Grammatical unification, A simple deduction method for modal logic, Principal type schemes for an extended type theory, Fundamental properties of infinite trees, Towards a programming language based on the notion of two-level grammar, Automated theorem proving methods, On the correspondence between two classes of reduction systems, Closures and fairness in the semantics of programming logic, Condensed detachment as a rule of inference, The two-property and condensed detachment, A superposition oriented theorem prover, A mechanical solution of Schubert's steamroller by many-sorted resolution, Refutational theorem proving using term-rewriting systems, Rewrite systems on a lattice of types, Is there an axiomatic semantics for standard pure Prolog?, Equational methods in first order predicate calculus, Simple second-order languages for which unification is undecidable, A resolution rule for well-formed formulae, Pattern-directed invocation with changing equations, The problem of choosing the type of subsumption to use, Double-negation elimination in some propositional logics, Group cancellation and resolution, A resolution principle for constrained logics, Completeness results for basic narrowing, On space and depth in resolution, A tableau-like proof procedure for normal modal logics, Annotations in formal specifications and proofs, Accelerating tableaux proofs using compact representations, On subsumption in distributed derivations, Problem solving by searching for models with a theorem prover, TWAM: a certifying abstract machine for logic programs, Proof strategies in linear logic, On the termination of clause graph resolution, A note on the proof theory of the \(\lambda \Pi\)-calculus, A note about \(k\)-DNF resolution, Resolution and the integrality of satisfiability problems, A numerical strategy to defectuous knowledge using, Automated theorem proving in mathematics., Embedding complex decision procedures inside an interactive theorem prover., An average case analysis of a resolution principle algorithm in mechanical theorem proving., The application of automated reasoning to questions in mathematics and logic, Unification: A case-study in data refinement, Definite clause programs are canonical (over a suitable domain), Polynomial-time inference of all valid implications for Horn and related formulae, A simplified form of condensed detachment, The anatomy of vampire. Implementing bottom-up procedures with code trees, Relating size and width in variants of Q-resolution, A finitely axiomatized formalization of predicate calculus with equality, Formalization of the resolution calculus for first-order logic, Induction using term orders, On Skolemization in constrained logics, Unification in sort theories and its applications, A BDD SAT solver for satisfiability testing: An industrial case study, TPS: A theorem-proving system for classical type theory, Jack Minker --- A profile, Reasoning with conditional axioms, Structured proof procedures, An order-sorted resolution in theory and practice, A temporal logic for real-time partial ordering with named transactions, On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic, Deciding the word problem in the union of equational theories., Resolution lower bounds for the weak functional pigeonhole principle., Extracting models from clause sets saturated under semantic refinements of the resolution rule., Clause trees: A tool for understanding and implementing resolution in automated reasoning, Improved algorithms for optimal length resolution refutation in difference constraint systems, Guest editor's introduction: JvH100, Editor's introduction to Jean van Heijenoort, ``Historical development of modern logic, Jean van Heijenoort's contributions to proof theory and its history, Comparing approaches to the exploration of the domain of residue classes., On the complexity of equational problems in CNF, Document models, Limits of theory sequences over algebraically closed fields and applications., Anderson and Belnap's invitation to sin, Note on the generalization of calculations, The \(Multi\)-SAT algorithm, Mixed logical-linear programming, Relaxed unification -- proposal, Derivation and inference of higher-order strictness types, Finding read-once resolution refutations in systems of 2CNF clauses, Proofs of a set of hybrid let-polymorphic type inference algorithms, Understanding cutting planes for QBFs, Finding models through graph saturation, Structuring and automating hardware proofs in a higher-order theorem- proving environment, A unification-theoretic method for investigating the \(k\)-provability problem, Logical knowledge-representation formalisms, Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic, Complete sets of unifiers and matchers in equational theories, Average-case analysis of Robinson's unification algorithm with two different variables, On the logic of unification, Horn equational theories and paramodulation, Boolean unification - the story so far, Basic narrowing revisited, On equational theories, unification, and (un)decidability, Unification in permutative equational theories is undecidable, A new fuzzy resolution principle based on the antonym, Similarities between powersets of terms, Universal abstract consistency class and universal refutation, The proof complexity of analytic and clausal tableaux, Proof-search in type-theoretic languages: An introduction, Deciding the \(E^+\)-class by an a posteriori, liftable order, The linked conjunct method for automatic deduction and related search techniques, Bounded arithmetic, proof complexity and two papers of Parikh, The \(Q^*\) algorithm - a search strategy for a deductive question-answering system, A method for the synthesis of deducibility conditions for Horn and some other formulas, Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas, Type reconstruction for linear \(\pi\)-calculus with I/O subtyping., A uniform procedure for converting matrix proofs into sequent-style systems, Working with ARMs: Complexity results on atomic representations of Herbrand models, The application of automated reasoning to formal models of combinatorial optimization, Tractable reasoning via approximation, A typed resolution principle for deduction with conditional typing theory, Reasoning, nonmonotonicity and learning in connectionist networks that capture propositional knowledge, A comparative study of open default theories, A linear and discrete programming framework for representing qualitative knowledge, Weighted systems of equations, Mixtus: An automatic partial evaluator for full Prolog, SET-VAR, \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations, Competing for the \(AC\)-unification race, Open and closed scopes for constrained genericity, On the mechanical derivation of loop invariants, Proving unsatisfiability of CNFs locally, Logic of temporal attribute implications, Lattices of polynomials under substitution, Transforming Boolean equalities into constraints, What we can learn from conflicts in propositional satisfiability, Types for modules, Type data bases with incomplete information, Category-sorted algebra-based action semantics, Proving Arrow's theorem by \texttt{PROLOG}, Counting for satisfiability by inverting resolution, An efficient labelled nested multiset unification algorithm, Generalizing DPLL and satisfiability for equalities, Code-carrying theories, \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality, General form of \(\alpha\)-resolution principle for linguistic truth-valued lattice-valued logic, Multiagent temporal logics, unification problems, and admissibilities, A simple proof of QBF hardness, Strong ETH and resolution via games and the multiplicity of strategies, Clean tangled clutters, simplices, and projective geometries, Towards a proof theory for quantifier macros, Projectivity and unification in substructural logics of generalized rotations, Integer feasibility and refutations in UTVPI constraints using bit-scaling, Contradiction separation based dynamic multi-clause synergized automated deduction, Resolution with order and selection for hybrid logics, Logical reduction of metarules, A taxonomy of exact methods for partial Max-SAT, The fuzzy logic programming language FASILL: design and implementation, First-order automated reasoning with theories: when deduction modulo theory meets practice, Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra, A characterization of tree-like resolution size, Closed form fuzzy interpolation, Towards a formal framework for heterogeneous relation algebra, Automatic synthesis of action programs for intelligent robots, The practicality of generating semantic trees for proofs of unsatisfiability, Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach, Solving SAT by algorithm transform of Wu's method, On the relevance of some families of fuzzy sets, \texttt{EVL}: a typed higher-order functional language for events, Towards a clausal analysis of cut-elimination, Solving equations with sequence variables and sequence functions, Partition-based logical reasoning for first-order and propositional theories, Knowledge-based proof planning, Visualizing SAT instances and runs of the DPLL algorithm, Copy complexity of Horn formulas with respect to unit read-once resolution, Unification in pretabular extensions of S4, Learning from interpretation transition, Extended resolution simulates binary decision diagrams, Cut-elimination: syntax and semantics, Markov logic networks, Space proof complexity for random 3-CNFs, A hybrid reasoning system for terminologies and first-order clauses in knowledge bases, Essential unifiers, Limitations of restricted branching in clause learning, Sequent forms of Herbrand theorem and their applications, Proof schemata in Hilbert-type axiomatic theories, The undecidability of the second order predicate unification problem, From LCF to Isabelle/HOL, Milestones from the Pure Lisp Theorem Prover to ACL2, Proving semantic properties as first-order satisfiability, Theoretical advances in artificial immune systems, Generating extended resolution proofs with a BDD-based SAT solver, \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments, Analyzing unit read-once refutations in difference constraint systems, Equational theorem proving modulo, Generalized completeness for SOS resolution and its application to a new notion of relevance, Inference approach based on Petri nets, A cube of opposition for predicate logic, Resolution graphs, Generalized means-ends analysis and artificial intelligence, The unit-clause proof procedure with equality, Extracting information from resolution proof trees, Finding resolution proofs and using duplicate goals in AND/OR trees, Formal methods in the design of question-answering systems, Experiments with a heuristic theorem-proving program for predicate calculus with equality, Computer proofs of limit theorems, Theorem proving with variable-constrained resolution, Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search, A note on linear resolution strategies in consequence-finding, Normal forms of conditional knowledge bases respecting system P-entailments and signature renamings, Beweisalgorithmen für die Prädikatenlogik, The application of the methods of the theory of logical derivation to graph theory, Breadth-first search: some surprising results, Synthesis of the resolution method with the inverse method, Hyperresolution for Gödel logic with truth constants, Weak linearization of the lambda calculus, Source-tracking unification, A general framework for types in graph rewriting, Distributive bilattices from the perspective of natural duality theory., Typical case complexity of satisfiability algorithms and the threshold phenomenon, Meta-interpretive learning as metarule specialisation, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, Faster linear unification algorithm, An efficient subsumption test pipeline for BS(LRA) clauses, Semantic relevance, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description), Projectivity in (bounded) commutative integral residuated lattices, SMELS: satisfiability modulo equality with lazy superposition, Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry, A proof builder for Max-SAT, Symbolic computation in Maude: some tapas, Automated Reasoning Building Blocks, To Vladimir Lifschitz on His 65th Birthday, Unnamed Item, Propositional SAT Solving, Transfer of Model Checking to Industrial Practice, Efficient Low-Level Connection Tableaux, On complexity of the anti-unification problem, Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable, Computational logic: its origins and applications, Logic programming as a service, Performing fully parallel constraint logic programming on a quantum annealer, Predicate invention and utilization, The undecidability of the DA-unification problem, A system of constructor classes: overloading and implicit higher-order polymorphism, Size-based termination of higher-order rewriting, Space Complexity in Polynomial Calculus, On First-Order Model-Based Reasoning, On the Parameterized Complexity of Associative and Commutative Unification, Direct deductive computation on discourse representation structures, Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’, Unnamed Item, Conjunctive Abstract Interpretation Using Paramodulation, Comparisons Among α-Generalized Resolution Methods in $$\fancyscript{L}_{n \times 2}$$F(X), Verification, validation, and integrity issues in expert and database systems: Two perspectives, Unnamed Item, Analytic tableaux for default logics, Coercions in a polymorphic type system, Unnamed Item, Meeting of the Association for Symbolic Logic, New York, 1974, Structuralism? Functionalism? Behaviorism? Or mechanism? Looking for a better approach to AI, Struktursätze der Algebra und Kompliziertheit logischer Schemata. III Algebraische Theorien und Verallgemeinerungen, Sémantique logique et dénotationnelle des interpréteurs PROLOG, Multi-ary α-semantic resolution automated reasoning based on lattice-valued first-order logic LF (X)1, On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas, Resolution-Like Theorem Proving for High-Level Conditions, Quantified Constraints in Twenty Seventeen, Unnamed Item, A partial solution for D-unification based on a reduction to AC 1-unification, An analysis of the Core-ML language: Expressive power and type reconstruction, Une approche intentionnelle du calcul des implicants premiers et essentiels des fonctions booléennes, Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems, What Is Essential Unification?, Logic and functional programming by retractions, Proof-terms for classical and intuitionistic resolution, Logical approach to control theory and applications, A Non-clausal Connection Calculus, Improving the time efficiency of proving theorems using a learning mechanism, T-string unification: Unifying prefixes in non-classical proof methods, A resolution theorem prover for intuitionistic logic, Converting non-classical matrix proofs into sequent-style systems, Advanced indexing operations on substitution trees, Semantic trees revisited: Some new completeness results, Search strategies for resolution in temporal logics, Path indexing for AC-theories, Unnamed Item, The Strategy Challenge in SMT Solving, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, The Relative Power of Semantics and Unification, First-Order Resolution Methods for Modal Logics, A Resolution-based Model Building Algorithm for a Fragment of OCC1N =, Horn clause computability, Lewis Carroll's Formal Logic, KNOWLEDGE REPRESENTATION: A SURVEY OF ITS MECHANISMS, A SKETCH OF ITS SEMANTICS, Type inference with simple subtypes, Partially Ordered Monads and Rough Sets, Removing irrelevant information in temporal resolution proofs, A Framework for Space Complexity in Algebraic Proof Systems, The design and application of structured types in Ptolemy II, Unnamed Item, A pragmatic approach to resolution-based theorem proving, Incremental and Modular Context-sensitive Analysis, Implementing Probabilistic Abductive Logic Programming with Constraint Handling Rules, Unnamed Item, Decidability of the unification problem for second-order languages with unary functional symbols, Unary Resolution: Characterizing Ptime, Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving, On the Hardness of SAT with Community Structure, Incremental Determinization, NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability, Unification with Singleton Tree Grammars, A Tutorial on Time and Space Bounds in Tree-Like Resolution, An Algorithm for Generating Arguments in Classical Predicate Logic, Type Inference for a Polynomial Lambda Calculus, The Resolution Method for 10-Element Linguistic Truth-Valued Propositional Logic, Formalization of the Resolution Calculus for First-Order Logic, Some (in)translatability results for normal logic programs and propositional theories, Abduction via C-tableaux and δ-resolution, Some applications of propositional logic to cellular automata, Combining Instance Generation and Resolution, A Class of Rewriting Rules and Reverse Transformation for Rule-based Equivalent Transformation, A categorical approach to unification of generalised terms1 1This work has been developed as a cooperation organised within COST 274., Conceptual modeling of data base operations, From Schütte’s Formal Systems to Modern Automated Deduction, Quantifier elimination and parametric polymorphism in programming languages, Lilac: a functional programming language based on linear logic, The complexity of type inference for higher-order typed lambda calculi, Polymorphic type, region and effect inference, MRPPS?An interactive refutation proof procedure system for question-answering, Representations of the language recognition problem for a theorem prover, Application of fuzzy logic to the detection of static hazards in combinational switching systems, A categorical formulation for critical-pair/completion procedures, A new approach to general E-unification based on conditional rewriting systems, An universal termination condition for solving goals in equational languages, Hardness Characterisations and Size-width Lower Bounds for QBF Resolution, Levy Labels and Recursive Types, Guarded horn clauses, Teaching Automated Theorem Proving by Example: PyRes 1.2, Seventy Years of Computer Science, Migrating gradual types, Proof normalization for resolution and paramodulation, Unification, weak unification, upper bound, lower bound, and generalization problems, Goal directed strategies for paramodulation, The negation elimination from syntactic equational formula is decidable, Substitution tree indexing, KoMeT, Decomposable theories, E-Unification based on Generalized Embedding, Logic programs with equational type specifications, Type inference in polymorphic type discipline, Role of logic programming in the FGCS project, Simplifying clausal satisfiability problems, Resolution in type theory, On CDCL-Based Proof Systems with the Ordered Decision Strategy, Type Inference for Rank 2 Gradual Intersection Types, Inference in Nineteenth-Century British Logic, Fifty Years of Prolog and Beyond, A Survey of the Proof-Theoretic Foundations of Logic Programming, Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic, Dynamic temporal logical operations in multi-agent logics, A formalised theorem in the partition calculus, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Analogical logic program synthesis algorithm that can refute inappropriate similarities, A multi-clause dynamic deduction algorithm based on standard contradiction separation rule, Typed SLD-resolution: dynamic typing for logic programming, Unifying splitting, Type inference for rank-2 intersection types using set unification, Sound and complete type inference for closed effect rows, Implementation of Makanin's Algorithm, Complete equational unification based on an extension of the Knuth-Bendix completion procedure, Never trust your solver: certification for SAT and QBF, Adding Negation to Lambda Mu, Depth lower bounds in Stabbing Planes for combinatorial principles, A (machine-oriented) logic based on pattern matching, Local confluence of conditional and generalized term rewriting systems, Admissibility and unification in the modal logics related to S4.2, On structures of regular standard contradictions in propositional logic, Towards automated deduction in cP systems, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Makanin's algorithm for word equations-two improvements and a generalization, Unit read-once refutations for systems of difference constraints, A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading, An algorithm for the retrieval of unifiers from discrimination trees, Unnamed Item, Unnamed Item, Inductive logic programming, Finding Effective SAT Partitionings Via Black-Box Optimization, Unification theory, Cut-elimination and redundancy-elimination by resolution, Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria, How to Produce Information About a Given Entity Using Automated Deduction Methods, Analogy in Automated Deduction: A Survey, From Boolean Equalities to Constraints, \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\), \(\alpha\)-resolution principle based on first-order lattice-valued logic \(\text{LF}(X)\), Unnamed Item, The complexity of resolution refinements, Proof-term synthesis on dependent-type systems via explicit substitutions, Results related to threshold phenomena research in satisfiability: Lower bounds, HM(X) type inference is CLP(X) solving, Parameterized Complexity of DPLL Search Procedures, Induction using term orderings, Detecting non-provable goals, Supercritical Space-Width Trade-offs for Resolution, On Herbrand's theorem, Proof Complexity of Non-classical Logics, The Complexity of Finding Read-Once NAE-Resolution Refutations, Unnamed Item, Unnamed Item, A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method, A practical integration of first-order reasoning and decision procedures, Exact knowledge compilation in predicate calculus: The partial achievement case, A classification of non-liftable orders for resolution, Complexity of translations from resolution to sequent calculus, A NON-DEFINABILITY RESULT FOR A PREDICATIONAL LANGUAGE WITH THE USUAL CONTROL, Normalization Issues in Mathematical Representations, Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK, A comprehensive framework for saturation theorem proving, Proofs and Certificates for Max-SAT, On simplifying the matrix of a wff, MaxSAT Resolution and Subcube Sums, Confluence of algebraic rewriting systems
