scientific article; zbMATH DE number 1500560

zbMATH Open0954.03011MaRDI QIDQ4501581FDOQ4501581

Authors: Koji Iwanuma, Kenichi Kishino 

Publication date: 4 September 2000

Title of this publication is not available (Why is that?)

Recommendations

• The use of lemmas in the model elimination procedure
• Lemma matching for a PTTP-based top-down theorem prover
• Lemma and cut strategies for propositional model elimination
• Persistent and quasi-persistent lemmas in propositional model elimination
• scientific article; zbMATH DE number 67452

zbMATH Keywords

accelerationmodel elimination calculuslemma facilitytop-down theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (6)

• Lemma matching for a PTTP-based top-down theorem prover
• First order Stålmarck. Universal lemmas through branch merges
• Persistent and quasi-persistent lemmas in propositional model elimination
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• OTTER

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 Q4501581)