A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics

AbstractIn 1984. Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidabie in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004. the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime. thus 2-ExpTime-complete. We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted on tree structures.

Download Full-text

Reasoning about Petri Nets: A Calculus Based on Resolution and Dynamic Logic

ACM Transactions on Computational Logic ◽

10.1145/3441655 ◽

2021 ◽

Vol 22 (2) ◽

pp. 1-22

Author(s):

Bruno Lopes ◽

Cláudia Nalon ◽

Edward Hermann Haeusler

Keyword(s):

Normal Form ◽

Petri Nets ◽

Dynamic Logic ◽

Concurrent Systems ◽

Modal Logics ◽

Inference Rules ◽

Logical Language ◽

Dynamic Logics

Petri Nets are a widely used formalism to deal with concurrent systems. Dynamic Logics (DLs) are a family of modal logics where each modality corresponds to a program. Petri-PDL is a logical language that combines these two approaches: it is a dynamic logic where programs are replaced by Petri Nets. In this work we present a clausal resolution-based calculus for Petri-PDL. Given a Petri-PDL formula, we show how to obtain its translation into a normal form to which a set of resolution-based inference rules are applied. We show that the resulting calculus is sound, complete, and terminating. Some examples of the application of the method are also given.

Download Full-text

Inference in action

Publications de l Institut Mathematique ◽

10.2298/pim0796003v ◽

2007 ◽

pp. 3-16 ◽

Cited By ~ 1

Author(s):

Benthem van

Keyword(s):

Classical Logic ◽

Recent Trend ◽

Dynamic Logic ◽

Substructural Logics ◽

Representation Theorems ◽

Cross Model ◽

Structural Rules ◽

Generalized Inference ◽

Information Update ◽

Dynamic Logics

Substructural logics arise whenever classical logic is put to new uses, and logicians from Serbia have been in the fore-front here. In this paper, we join the substructural tradition with another recent trend, viz. dynamic logic of information update. We show how these two approaches fit together in particular, through a number of representation theorems concerning structural rules. The proper background for these results turn out to be modal and dynamic logics of cross-model relations. We connect this finding with recent accounts of generalized inference, interpolation, and preservation results.

Download Full-text

A Comparison of Solvers for Propositional Dynamic Logic

10.29007/63hq ◽

2018 ◽

Author(s):

Ullrich Hustadt ◽

Renate A. Schmidt

Keyword(s):

Dynamic Logic ◽

Propositional Dynamic Logic ◽

Dynamic Logics

Calculi for propositional dynamic logics have been investigated since the introduction of this logic in the late seventies. Only in recent years have practical procedures been suggested and implemented. In this paper, we compare three such systems, namely, the Tableau Workbench by Abate, Gore, and Widmann (2009), the pdlProver system by Gore and Widmann (2009), and the MLSolver system by Friedmann and Lange (2009).

Download Full-text

Decidability and Complexity of Some Finitely-valued Dynamic Logics

10.24963/kr.2021/54 ◽

2021 ◽

Author(s):

Igor Sedlár

Keyword(s):

Transitive Closure ◽

Description Logics ◽

Dynamic Logic ◽

Time Algorithm ◽

Action Execution ◽

Propositional Dynamic Logic ◽

Relational Models ◽

Reasoning About Actions ◽

Decidability And Complexity ◽

Dynamic Logics

Propositional Dynamic Logic, PDL, is a well known modal logic formalizing reasoning about complex actions. We study many-valued generalizations of PDL based on relational models where satisfaction of formulas in states and accessibility between states via action execution are both seen as graded notions, evaluated in a finite Łukasiewicz chain. For each n>1, the logic PDŁn is obtained using the n-element Łukasiewicz chain, PDL being equivalent to PDŁ2. These finitely-valued dynamic logics can be applied in formalizing reasoning about actions specified by graded predicates, reasoning about costs of actions, and as a framework for certain graded description logics with transitive closure of roles. Generalizing techniques used in the case of PDL we obtain completeness and decidability results for all PDŁn. A generalization of Pratt's exponential-time algorithm for checking validity of formulas is given and EXPTIME-hardness of each PDŁn validity problem is established by embedding PDL into PDŁn.

Download Full-text

Low Power Wide Fan-in Domino OR Gate Using CN-MOSFETs

International Journal of Sensors Wireless Communications and Control ◽

10.2174/2210327909666190207163639 ◽

2020 ◽

Vol 10 (1) ◽

pp. 55-62

Author(s):

Deepika Bansal ◽

Bal Chand Nagar ◽

Brahamdeo Prasad Singh ◽

Ajay Kumar

Keyword(s):

Power Consumption ◽

High Performance ◽

Dynamic Logic ◽

Clock Frequency ◽

Charge Sharing ◽

Benchmark Circuit ◽

Domino Circuit ◽

Power Delay Product ◽

Domino Circuits ◽

Or Gate

Background & Objective: In this paper, a modified pseudo domino configuration has been proposed to improve the leakage power consumption and Power Delay Product (PDP) of dynamic logic using Carbon Nanotube MOSFETs (CN-MOSFETs). The simulations for proposed and published domino circuits are verified by using Synopsys HSPICE simulator with 32nm CN-MOSFET technology which is provided by Stanford. Methods: The simulation results of the proposed technique are validated for improvement of wide fan-in domino OR gate as a benchmark circuit at 500 MHz clock frequency. Results: The proposed configuration is suitable for cascading of the high performance wide fan-in circuits without any charge sharing. Conclusion: The performance analysis of 8-input OR gate demonstrate that the proposed circuit provides lower static and dynamic power consumption up to 62 and 40% respectively, and PDP improvement is 60% as compared to standard domino circuit.

Download Full-text

On Sequential Form of Functional Dynamic Logics

Fundamenta Informaticae ◽

10.3233/fi-1984-7310 ◽

1984 ◽

Vol 7 (3) ◽

pp. 357-358

Author(s):

Regimantas Pliuškevičius

Keyword(s):

Axiom Systems ◽

Dynamic Logics

A Gentzen-style axiomatization of dynamic logics is proposed. It is compared to other axiom systems for dynamic logics. Some problems of relative decidability are considered.

Download Full-text