A proof strategy based on a dual representation

DOI10.1007/3-540-44990-6_6MaRDI QIDQ4471941zbMATH OpenFDO

Authors Guilherme Bittencourt, Isabel Tonin

Publication date 30 July 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/1930/19300078.htm

zbMATH Keywords

dual transformationFirst-order logicinference strategytheorem proving

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4170865
• On some strategies of logical inference search that are driven by goals
• Concurrent inference through dual transformation
• The search efficiency of theorem proving strategies
• Resolution theorem proving

Cited in

(6)

• A study of an integrated proof strategy
• On some strategies of logical inference search that are driven by goals
• Strategies. What's in a name?
• scientific article; zbMATH DE number 4170865 (Why is no real title available?)
• Concurrent inference through dual transformation
• An algorithm for dual transformation in first-order logic

Describes a project that uses

Uses Software

• Ivy

This page was built for publication: A proof strategy based on a dual representation

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