Publication:3743300
From MaRDI portal
zbMath0605.03004MaRDI QIDQ3743300
Publication date: 1986
PROLOG; proof theory; resolution; logic programming; proof systems; Gentzen systems; automatic theorem proving; algorithmic methods
03-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
03B35: Mechanization of proofs and logical operations
68-02: Research exposition (monographs, survey articles) pertaining to computer science
03F99: Proof theory and constructive mathematics
Related Items
Frege and the resolution calculus, Increasing the efficiency of automated theorem proving, Connecting many-sorted theories, Proofs as computations in linear logic, Unification in a combination of arbitrary disjoint equational theories, Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, 3-SAT = SAT for a class of normal modal logics, R-calculus for ELP: An operational approach to knowledge base maintenance, Parsing as non-Horn deduction, Negation in rule-based database languages: A survey, Negation by default and unstratifiable logic programs, Using forcing to prove completeness of resolution and paramodulation, Optimizing the clausal normal form transformation, Order-sorted logic programming with predicate hierarchy, NP-containment for the coherence test of assessments of conditional probability: a fuzzy logical approach, Rigid E-unification: NP-completeness and applications to equational matings, A semantic approach to interpolation, The RISC ProofNavigator: a proving assistant for program verification in the classroom, Quantified coalition logic, Resolution on formula-trees, Fast algorithms for testing unsatisfiability of ground Horn clauses with equations, The power of temporal proofs, Higher-order rewrite systems and their confluence, Fuzzy term-rewriting system, A semantic backward chaining proof system, A method for simultaneous search for refutations and models by equational constraint solving, Existential instantiation and normalization in sequent natural deduction, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, A key to fuzzy-logic inference, A new method for undecidability proofs of first order theories, Partial logics reconsidered: A conservative approach, Complete sets of transformations for general E-unification, Representing scope in intuitionistic deductions, Gentzen-type systems, resolution and tableaux, Unique complements and decompositions of database schemata, A resolution principle for constrained logics, Proof rules for recursive procedures, A term equality problem equivalent to graph isomorphism, Min-max functions, On proof normalization in linear logic, The saturated tableaux for linear miniscope Horn-like temporal logic, Using automata theory for characterizing the semantics of terminological cycles, Intuitive minimal abduction in sequent calculi, A programmable approach to maintenance of a finite knowledge base, Fast algorithms for revision of some special propositional knowledge bases, Theorem proving modulo, Proof-search in type-theoretic languages: An introduction, Operational and complete approaches to belief revision, Structuring and automating hardware proofs in a higher-order theorem- proving environment, On the logic of unification, Higher-order unification revisited: Complete sets of transformations, Linear concurrent constraint programming: Operational and phase semantics, A general framework for reasoning about change, Pattern matching as cut elimination, Middle-out reasoning for synthesis and induction, Counting for satisfiability by inverting resolution, Decision procedures for extensions of the theory of arrays, Sequent forms of Herbrand theorem and their applications, Formal verification of a generic framework to synthesize SAT-provers, On Extended Regular Expressions, Can we transform logic programs into attribute grammars ?, Intuitionistic three-valued logic and logic programming
