scientific article; zbMATH DE number 1500560

MaRDI QIDQ4501581zbMATH OpenFDO

Authors Koji Iwanuma, Kenichi Kishino

Publication date 4 September 2000

zbMATH Keywords

accelerationmodel elimination calculuslemma facilitytop-down theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

Cited in

(6)

• scientific article; zbMATH DE number 1612567 (Why is no real title available?)
• Persistent and quasi-persistent lemmas in propositional model elimination
• scientific article; zbMATH DE number 67452 (Why is no real title available?)
• First order Stålmarck. Universal lemmas through branch merges
• scientific article; zbMATH DE number 6785324 (Why is no real title available?)
• Lemma matching for a PTTP-based top-down theorem prover

Describes a project that uses

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)