scholarly journals Interpolant based Decision Procedure for Quantifier-Free Presburger Arithmetic

2007 ◽  
Vol 1 (3-4) ◽  
pp. 187-207
Author(s):  
Shuvendu K. Lahiri ◽  
Krishna K. Mehra
Keyword(s):  
Decision Procedure ◽  
Presburger Arithmetic

A Decision Procedure for Bit-Vector Arithmetic

1998 ◽  
Author(s):  
Clark W. Barrett ◽  
David L. Dill ◽  
Jeremy R. Levitt
Keyword(s):  
Decision Procedure ◽  
Bit Vector

An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until1

1992 ◽  
Vol 17 (3) ◽  
pp. 271-282
Author(s):  
Y.S. Ramakrishna ◽  
L.E. Moser ◽  
L.K. Dillon ◽  
P.M. Melliar-Smith ◽  
G. Kutty
Keyword(s):  
Temporal Logic ◽  
Decision Procedure ◽  
Linear Time ◽  
Computer Systems ◽  
Hierarchical Abstraction ◽  
Soundness And Completeness

We present an automata-theoretic decision procedure for Since/Until Temporal Logic (SUTL), a linear-time propositional temporal logic with strong non-strict since and until operators. The logic, which is intended for specifying and reasoning about computer systems, employs neither next nor previous operators. Such operators obstruct the use of hierarchical abstraction and refinement and make reasoning about concurrency difficult. A proof of the soundness and completeness of the decision procedure is given, and its complexity is analyzed.

scholarly journals Periodic behavior in families of numerical and affine semigroups via parametric Presburger arithmetic

2021 ◽  
Vol 102 (2) ◽  
pp. 340-356
Author(s):  
Tristram Bogart ◽  
John Goodrick ◽  
Kevin Woods
Keyword(s):  
Periodic Behavior ◽  
Presburger Arithmetic ◽  
Affine Semigroups

Deciding Clause Classes by Semantic Clash Resolution

1993 ◽  
Vol 18 (2-4) ◽  
pp. 163-182
Author(s):  
Alexander Leitsch
Keyword(s):  
Decision Procedure ◽  
Decision Procedures ◽  
General Concept ◽  
Complexity Measure ◽  
Syntactical Structure

It is investigated, how semantic clash resolution can be used to decide some classes of clause sets. Because semantic clash resolution is complete, the termination of the resolution procedure on a class Γ gives a decision procedure for Γ. Besides generalizing earlier results we investigate the relation between termination and clause complexity. For this purpose we define the general concept of atom complexity measure and show some general results about termination in terms of such measures. Moreover, rather than using fixed resolution refinements we define an algorithmic generator for decision procedures, which constructs appropriate semantic refinements out of the syntactical structure of the clause sets. This method is applied to the Bernays – Schönfinkel class, where it gives an efficient (resolution) decision procedure.

The Legislative Impact of the European Parliament Under the Revised Co-Decision Procedure

2004 ◽  
Vol 5 (2) ◽  
pp. 241-260 ◽  
Author(s):  
Christiane Kasack
Keyword(s):  
Decision Procedure ◽  
European Parliament

Relational dual tableau decision procedure for modal logic K

2011 ◽  
Vol 20 (4) ◽  
pp. 747-756 ◽  
Author(s):  
J. Golinska-Pilarek ◽  
E. Munoz-Velasco ◽  
A. Mora-Bonilla
Keyword(s):  
Modal Logic ◽  
Decision Procedure
Sign in / Sign up

Export Citation Format

Share Document