A certified polynomial-based decision procedure for propositional logic

DOI10.1007/3-540-44755-5_21MaRDI QIDQ4790667zbMATH OpenFDO

Authors Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez

Publication date 4 February 2003

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/2152/21520297

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• On polynomial semantics for propositional logics
• A decision procedure for univariate polynomial systems based on root counting and interval subdivision
• Deciding polynomial-exponential problems
• Automating the synthesis of decision procedures in a constructive metatheory
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL

Cited in

(4)

• Polynomial algorithm of limited propositional deduction
• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• scientific article; zbMATH DE number 2127871 (Why is no real title available?)
• A decision procedure for univariate polynomial systems based on root counting and interval subdivision

Describes a project that uses

Uses Software

• ACL2
• Coq
• HOL

This page was built for publication: A certified polynomial-based decision procedure for propositional logic

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