Logic programming approach to automata-based decision procedures

DOI10.1016/J.JLAMP.2016.02.005MaRDI QIDQ347398zbMATHOpenAlexFDO

Authors Gulay Unel, David Toman

Publication date 30 November 2016

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2016.02.005

zbMATH Keywords

automatacomplex-value Datalog \((\text{Datalog}^{\text{cv}})\)magic setsSLG-resolutionWS1SWS2S

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Logic programming (68N17) Decidability of theories and sets of sentences (03B25)

Recommendations

• Logic Programming Approach to Automata-Based Decision Procedures
• Lazy automata techniques for WS1S
• Publication:4783320
• MONA IMPLEMENTATION SECRETS
• An Incremental Technique for Automata-Based Decision Procedures

Cites work

• scientific article; zbMATH DE number 1670781 (Why is no real title available?)
• scientific article; zbMATH DE number 3972842 (Why is no real title available?)
• scientific article; zbMATH DE number 1223628 (Why is no real title available?)
• scientific article; zbMATH DE number 1223729 (Why is no real title available?)
• scientific article; zbMATH DE number 1332641 (Why is no real title available?)
• scientific article; zbMATH DE number 1786477 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 2102710 (Why is no real title available?)
• scientific article; zbMATH DE number 839556 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
• Alternating automata: unifying truth and validity checking for temporal logics
• An automata theoretic decision procedure for the propositional mu- calculus
• An automata-theoretic approach to branching-time model checking
• Automata for the modal \(\mu \)-calculus and related results
• Automata, logics, and infinite games. A guide to current research
• BDD-based decision procedures for the modal logic K ★
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Deciding entailments in inductive separation logic with tree automata
• Deciding full branching time logic
• Decision Problems of Finite Automata Design and Related Arithmetics
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Logic Programming Approach to Automata-Based Decision Procedures
• MONA IMPLEMENTATION SECRETS
• On model checking for the \(\mu\)-calculus and its fragments
• On the power of magic
• Reasoning about infinite computations
• Set constructors in a logic database language
• Testing and generating infinite sequences by a finite automaton
• The Description Logic Handbook
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(3)

• Logic Programming Approach to Automata-Based Decision Procedures
• An Incremental Technique for Automata-Based Decision Procedures
• Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic

Describes a project that uses

Uses Software

• MONA
• LTL2BA
• XSB
• Slide
• MSO_Regex_Equivalence

This page was built for publication: Logic programming approach to automata-based decision procedures

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