scientific article; zbMATH DE number 3666758
From MaRDI portal
Publication:3864488
semantic tableauxcompactness theoremsequentLISPKönig's lemmaclausal transformHerbrand mapmechanization of deductive reasoningvaluation of sentences
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) History of mathematical logic and foundations (03-03) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Cited in
(22)- Implementing the `Fool's model' of combinatory logic
- A (machine-oriented) logic based on pattern matching
- Condensed detachment as a rule of inference
- On the relation between default and autoepistemic logic
- Completeness results for inequality provers
- Intuitionistic hybrid logic: introduction and survey
- Completeness of resolution revisited
- Solving problems with automated reasoning, expert systems and neural networks
- Jean van Heijenoort's contributions to proof theory and its history
- Resolution theorem proving in reified modal logics
- Grammatical unification
- A cube of opposition for predicate logic
- Relevant logic programming
- Simplification in a satisfiability checker for VLSI applications
- History and basic features of the critical-pair/completion procedure
- Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic
- Editor's introduction to Jean van Heijenoort, ``Historical development of modern logic
- Guest editor's introduction: JvH100
- Monads for the formalization of a pattern matching procedure
- Gentzen-type systems, resolution and tableaux
- The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
- Frege and the resolution calculus
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 Q3864488)
