scientific article

Publication date: 1986

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

PROLOG proof theory resolution logic programming proof systems Gentzen systems automatic theorem proving algorithmic methods

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Proof theory and constructive mathematics (03F99)

Related Items

Provability multilattice logic ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ A novel approach to equality ⋮ A Comparison of Sets of Recognizable Weighted Tree Languages Over Specific Sets of Bounded Lattices ⋮ Proofs as computations in linear logic ⋮ SAT-Inspired Eliminations for Superposition ⋮ A resolution principle for constrained logics ⋮ Proof rules for recursive procedures ⋮ Soundness and completeness proofs by coinductive methods ⋮ A general framework for reasoning about change ⋮ A term equality problem equivalent to graph isomorphism ⋮ Evidence algorithm and inference search in first-order logics ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Pattern matching as cut elimination ⋮ Min-max functions ⋮ The undecidability of proof search when equality is a logical connective ⋮ Modeling Complex Systems and Their Validation—General System Theoretical Approach ⋮ On proof normalization in linear logic ⋮ On process equivalence = equation solving in CCS ⋮ Connecting many-sorted theories ⋮ The saturated tableaux for linear miniscope Horn-like temporal logic ⋮ Computing ground reducibility and inductively complete positions ⋮ Efficient ground completion ⋮ Goal directed strategies for paramodulation ⋮ A note on cut-elimination for classical propositional logic ⋮ Resolution on formula-trees ⋮ A logic and computation for Popper's conditional probabilities ⋮ Fast algorithms for testing unsatisfiability of ground Horn clauses with equations ⋮ Term-Generic Logic ⋮ Can we transform logic programs into attribute grammars ? ⋮ Intuitionistic three-valued logic and logic programming ⋮ Counting for satisfiability by inverting resolution ⋮ Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable ⋮ \textbf{R}-calculus without the cut rule ⋮ Tautology Elimination, Cut Elimination, and S5 ⋮ Middle-out reasoning for synthesis and induction ⋮ Maximal contractions in Boolean algebras ⋮ The power of temporal proofs ⋮ Increasing the efficiency of automated theorem proving ⋮ NP-containment for the coherence test of assessments of conditional probability: a fuzzy logical approach ⋮ Using automata theory for characterizing the semantics of terminological cycles ⋮ Higher-order rewrite systems and their confluence ⋮ Applying term rewriting methods to finite groups ⋮ Intuitive minimal abduction in sequent calculi ⋮ LINEAR TIME IN HYPERSEQUENT FRAMEWORK ⋮ Some general results about proof normalization ⋮ A programmable approach to maintenance of a finite knowledge base ⋮ Keeping logic in the trivium of computer science: a teaching perspective ⋮ A semantic framework for proof evidence ⋮ Extracting the resolution algorithm from a completeness proof for the propositional calculus ⋮ A sequent calculus for reasoning in four-valued Description Logics ⋮ Fast algorithms for revision of some special propositional knowledge bases ⋮ Unnamed Item ⋮ Rigid E-unification: NP-completeness and applications to equational matings ⋮ Theorem proving modulo ⋮ Decision procedures for extensions of the theory of arrays ⋮ Fuzzy term-rewriting system ⋮ 3-SAT = SAT for a class of normal modal logics ⋮ Frege and the resolution calculus ⋮ R-calculus for ELP: An operational approach to knowledge base maintenance ⋮ The incremental satisfiability problem for a two conjunctive normal form ⋮ 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 ⋮ Parsing as non-Horn deduction ⋮ Bayesian updating rules and AGM belief revision ⋮ 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 ⋮ An algorithm to compute maximal contractions for Horn clauses ⋮ Formal SOS-Proofs for the Lambda-Calculus ⋮ Regaining cut admissibility in deduction modulo using abstract completion ⋮ Sequent forms of Herbrand theorem and their applications ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ Tools for proving inductive equalities, relative completeness, and $\omega$-completeness ⋮ The $\lambda $-calculus and the unity of structural proof theory ⋮ Axiomatization of Typed First-Order Logic ⋮ On Extended Regular Expressions ⋮ Structuring and automating hardware proofs in a higher-order theorem- proving environment ⋮ A semantic approach to interpolation ⋮ Model elimination without contrapositives ⋮ On intuitionistic query answering in description bases ⋮ Partial logics reconsidered: A conservative approach ⋮ Complete sets of transformations for general E-unification ⋮ A representation of proper BC domains based on conjunctive sequent calculi ⋮ The RISC ProofNavigator: a proving assistant for program verification in the classroom ⋮ Negation in rule-based database languages: A survey ⋮ Negation by default and unstratifiable logic programs ⋮ Quantified coalition logic ⋮ Using forcing to prove completeness of resolution and paramodulation ⋮ Representing scope in intuitionistic deductions ⋮ Foundations of the rule-based system ρLog ⋮ On the logic of unification ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver ⋮ Automating Theories in Intuitionistic Logic ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Operational and complete approaches to belief revision ⋮ Term-generic logic ⋮ Linear concurrent constraint programming: Operational and phase semantics ⋮ Formal verification of a generic framework to synthesize SAT-provers ⋮ Gentzen-type systems, resolution and tableaux ⋮ Optimizing the clausal normal form transformation ⋮ Unique complements and decompositions of database schemata ⋮ THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY ⋮ Order-sorted logic programming with predicate hierarchy