An algorithm for dual transformation in first-order logic

DOI10.1023/A:1011917032470MaRDI QIDQ5956118zbMATH OpenFDO

Authors Guilherme Bittencourt, Isabel Tonin

Publication date 19 February 2002

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/A:1011917032470

zbMATH Keywords

concurrent algorithmdual transformationfirst-order logicknowledge representationtheorem provingtransformation between conjunctive and disjunctive canonical forms

Mathematics Subject Classification ID

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

Recommendations

• Concurrent inference through dual transformation
• scientific article; zbMATH DE number 3864540
• Optimizing the clausal normal form transformation
• scientific article; zbMATH DE number 404251
• scientific article; zbMATH DE number 2079834

Cited in

(5)

• A transformation scheme for infinitary first-order combinatorics presenting computational level of expressiveness in predicate logic
• scientific article; zbMATH DE number 3864540 (Why is no real title available?)
• Concurrent inference through dual transformation
• Minimizing disjunctive normal forms of pure first-order logic
• scientific article; zbMATH DE number 2135666 (Why is no real title available?)

Describes a project that uses

Uses Software

• LISP

This page was built for publication: An algorithm for dual transformation in first-order logic

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