Evidence algorithm and inference search in first-order logics

DOI10.1007/S10817-015-9346-0zbMATH1356.03055OpenAlexW2172979345MaRDI QIDQ286802FDOQ286802

Authors Alexander Lyaletski

Publication date 26 May 2016

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

Full work available at URL https://doi.org/10.1007/s10817-015-9346-0

zbMATH Keywords

first-order logicintuitionistic logicmodal logicsequent calculusautomated theorem provingclash-resolution methodclassical logicevidence algorithminference searchMaslov's inverse method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Recommendations

• Publication:4938416
• Publication:3682462
• Mathematical text processing in EA-style: a sequent aspect
• Evidence algorithm and system for automated deduction: a retrospective view. (In honor of 40 years of the EA announcement)
• Publication:3496309

Cites work

• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 3654113 (Why is no real title available?)
• scientific article; zbMATH DE number 3654114 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 2079533 (Why is no real title available?)
• scientific article; zbMATH DE number 1361537 (Why is no real title available?)
• scientific article; zbMATH DE number 3441640 (Why is no real title available?)
• scientific article; zbMATH DE number 1405443 (Why is no real title available?)
• scientific article; zbMATH DE number 3344563 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• scientific article; zbMATH DE number 3415412 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A free variable sequent calculus with uniform variable splitting
• A variant of Herbrand's theorem for formulas in prenex form
• Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system
• Evidential paradigm: the logical aspect
• Mathematical Knowledge Management
• Some problems in the theories of automata and artificial intelligence
• Untersuchungen über das logische Schliessen. I
• What is the inverse method?

Cited in

(7)

• Mathematical text processing in EA-style: a sequent aspect
• Evidential paradigm: the logical aspect
• Evidence algorithm and SAD systems: past and possible future
• scientific article; zbMATH DE number 1405443 (Why is no real title available?)
• Evidential support logic programming
• Logical analysis of emotions in text from natural language
• Evidence algorithm and system for automated deduction: a retrospective view. (In honor of 40 years of the EA announcement)

Describes a project that uses

Uses Software

• Mizar
• SAD
• ForTheL

This page was built for publication: Evidence algorithm and inference search in first-order logics

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