scientific article; zbMATH DE number 1323296

MaRDI QIDQ4255135zbMATH OpenFDO

Authors Sunna Torge

Publication date 10 August 1999

zbMATH Keywords

automated reasoningexistential quantifiersextended-positive-tableaux-methodfinite satisfiabilityimplementation in Prologresolutionsatisfiable integrity constraintsunsatisfiability

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Recommendations

• A more efficient tableaux procedure for simultaneous search for refutations and finite models
• A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
• More on trees and finite satisfiability: The taming of terms
• Pruning the search space and extracting more models in tableaux

Cited in

(9)

• More on trees and finite satisfiability: The taming of terms
• Finite verification of the characteristic specification of discrete systems
• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
• A Function Elimination Method for Checking Satisfiability of Arithmetical Logics
• scientific article; zbMATH DE number 4088977 (Why is no real title available?)
• scientific article; zbMATH DE number 1241716 (Why is no real title available?)
• scientific article; zbMATH DE number 1301750 (Why is no real title available?)
• Determination of the class of validity of logical formulas by directed exhaustive search
• Verification, induction, termination analysis. Festschrift for Christoph Walther on the occasion of his 60th birthday

Describes a project that uses

Uses Software

• FINDER

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 Q4255135)