scientific article; zbMATH DE number 3976991

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

Recommendations

Logic for computer scientists
scientific article; zbMATH DE number 837700
scientific article; zbMATH DE number 708485
scientific article; zbMATH DE number 46359
scientific article; zbMATH DE number 976352

Cited in

(only showing first 100 items - show all)

A semantic approach to interpolation
The RISC ProofNavigator: a proving assistant for program verification in the classroom
Quantified coalition logic
\texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
DFC-algorithms for Suszko logic and one-to-one Gentzen type formalizations
Resolution on formula-trees
Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
The power of temporal proofs
Unsolvable systems of equations and proof complexity
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
Automated deduction. A basis for applications. Vol. 1: Foundations, calculi and methods
Keeping logic in the trivium of computer science: a teaching perspective
A semantic framework for proof evidence
The incremental satisfiability problem for a two conjunctive normal form
Bayesian updating rules and AGM 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
Some general results about proof normalization
The undecidability of proof search when equality is a logical connective
A note on cut-elimination for classical propositional logic
A logic and computation for Popper's conditional probabilities
Fundamentals of logic and computation. With practical automated reasoning and verification
Regaining cut admissibility in deduction modulo using abstract completion
Term-generic logic
Soundness and completeness proofs by coinductive methods
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
scientific article; zbMATH DE number 1705882 (Why is no real title available?)
Evidence algorithm and inference search in first-order logics
Interpolation systems for ground proofs in automated deduction: a survey
Term-Generic Logic
A simple functional presentation and an inductive correctness proof of the Horn algorithm
\textbf{R}-calculus without the cut rule
On Extended Regular Expressions
Maximal contractions in Boolean algebras
Foundations of the rule-based system $\rho\,\text{Log}$
Automating theories in intuitionistic logic
Some Remarks on Theorem Proving Systems and Mazurkiewicz Algorithms Associated with them
scientific article; zbMATH DE number 4056963 (Why is no real title available?)
Can we transform logic programs into attribute grammars ?
Intuitionistic three-valued logic and logic programming
scientific article; zbMATH DE number 46359 (Why is no real title available?)
scientific article; zbMATH DE number 708485 (Why is no real title available?)
Frege and the resolution calculus
Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable
Tautology elimination, cut elimination, and S5
An encyclopaedia of proof systems
A sequent calculus for reasoning in four-valued description logics
scientific article; zbMATH DE number 2176109 (Why is no real title available?)
Increasing the efficiency of automated theorem proving
scientific article; zbMATH DE number 837700 (Why is no real title available?)
The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
Modeling complex systems and their validation -- general system theoretical approach
Some applications of Gentzen's proof theory in automated deduction
Computing ground reducibility and inductively complete positions
Efficient ground completion
Goal directed strategies for paramodulation
Applying term rewriting methods to finite groups
Formal SOS-Proofs for the Lambda-Calculus
Axiomatization of typed first-order logic
Model elimination without contrapositives
On intuitionistic query answering in description bases
A representation of proper BC domains based on conjunctive sequent calculi
Connecting many-sorted theories
LINEAR TIME IN HYPERSEQUENT FRAMEWORK
Fundamental proof methods in computer science. A computer-based approach
An algorithm to compute maximal contractions for Horn clauses
Unification in a combination of arbitrary disjoint equational theories

This page was built for publication:

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