scientific article; zbMATH DE number 3935002
From MaRDI portal
Publication:3708773
zbMATH Open0584.03008MaRDI QIDQ3708773FDOQ3708773
Authors: Charles G. Morgan 
Publication date: 1985
Title of this publication is not available (Why is that?)
Recommendations
implementationbackward proof tree generationlogics with modus ponensnon-resolutional theorem proving
Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Cited In (24)
- Backward reasoning in systems with cut
- Title not available (Why is that?)
- Automatic theorem proving and OTTER
- A nucleus of a theorem-prover described inAlgol-68
- Representing scope in intuitionistic deductions
- On flattening elimination rules
- Cut for classical core logic
- The relevance of premises to conclusions of core proofs
- Poitín: distilling theorems from conjectures
- Lazy techniques for fully expansive theorem proving
- Admissibility of structural rules for contraction-free systems of intuitionistic logic
- Title not available (Why is that?)
- A complete semantic back chaining proof system
- On Theorem Proving in Annotated Logics
- Title not available (Why is that?)
- The t‐variable method in gentzen‐style automatic theorem proving
- Title not available (Why is that?)
- The applicability of logic program analysis and transformation to theorem proving
- Title not available (Why is that?)
- Gentzen's proof systems: byproducts in a work of genius
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A new application for explanation-based generalisation within automated deduction
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 Q3708773)
