We propose a mechanism for automating discovery of definitions, that, when added to a logic system for which we have a theorem prover, extends it to support an embedding of a new logic system into it. As a result, the...
详细信息
ISBN:
(数字)9783030684464
ISBN:
(纸本)9783030684457;9783030684464
We propose a mechanism for automating discovery of definitions, that, when added to a logic system for which we have a theorem prover, extends it to support an embedding of a new logic system into it. As a result, the synthesized definitions, when added to the prover, implement a prover for the new logic. As an instance of the proposed mechanism, we derive a Prolog theorem prover for an interesting but unconventional epistemic logic by starting from the sequent calculus G4IP that we extend with operator definitions to obtain an embedding in intuitionistic propositional logic (IPC). With help of a candidate definition formula generator, we discover epistemic operators for which axioms and theorems of Artemov and Protopopescu's Intuitionistic Epistemic logic (IEL) hold and formulas expected to be non-theorems fail. We compare the embedding of IEL in IPC with a similarly discovered successful embedding of Dosen's double negation modality, judged inadequate as an epistemic operator. Finally, we discuss the failure of the necessitation rule for an otherwise successful S4 embedding and share our thoughts about the intuitions explaining these differences between epistemic and alethic modalities in the context of the Brouwer-Heyting-Kolmogorov semantics of intuitionistic reasoning and knowledge acquisition.
Unification algorithms of nominal expressions with letrec and atom- and expression-variables are already described in the literature. However, only explicit environments could be treated in nominal unification and the...
详细信息
ISBN:
(数字)9783030684464
ISBN:
(纸本)9783030684457;9783030684464
Unification algorithms of nominal expressions with letrec and atom- and expression-variables are already described in the literature. However, only explicit environments could be treated in nominal unification and the use of abstract environments was restricted to nominal matching. this severely restricts the use of algorithms in applications. the following two restrictions permit a step forward and strongly improve the coverage of the application cases: expression- and environment-variables are restricted to occur at most once in the input equations. A terminating and complete nominal unification algorithm is described that computes complete sets of constrained unifiers. Since the set of ground instances of a complete set may be empty due to constraints, we also provide a decision algorithm for inputs which do not contain permutation-variables and show that then nominal unifiability is NP-complete. For input without an occurrence-restriction for expression-variables and w.r.t. garbage-free ground expressions, we sketch an adapted unification algorithm that produces a complete set of unifiers in NP time. For the decision problem we conjecture that it is harder in this case. We believe that lifting the linearity restrictions for environment-variables leads to a prohibitively high computational complexity.
logic-basedprogramsynthesis and transformation : 8thinternationalworkshop, Lopstr'98, Manchester, Uk, June 15-19, 1998 : Selected Papers by internationalworkshop on logic-basedprogramsynthesis; Transformati...
详细信息
logic-basedprogramsynthesis and transformation : 8thinternationalworkshop, Lopstr'98, Manchester, Uk, June 15-19, 1998 : Selected Papers by internationalworkshop on logic-basedprogramsynthesis; transformation (8th : 1998 : Manchester, England); Flener, Pierre, 1964-; published by Berlin ; New York : Springer
the proceedings contain 11 papers. the topics discussed include: VICToRy: visual interactive consistency management in tolerant rule-based systems;graph repair and its application to meta-modeling;modeling adverse con...
the proceedings contain 11 papers. the topics discussed include: VICToRy: visual interactive consistency management in tolerant rule-based systems;graph repair and its application to meta-modeling;modeling adverse conditions in the framework of graph transformation systems;an algebraic graph transformation approach for RDF and SPARQL;graph surfing in reaction systems from a categorical perspective;encoding incremental NACs in safe graph grammars using complementation;weak Greibach normal form for hyperedge replacement grammars;efficient computation of graph overlaps for rule composition: theory and Z3 prototyping;reversibility and composition of rewriting in hierarchies;a fast graph program for computing minimum spanning trees;and verifying graph programs with first-order logic.
Nowadays, many critical systems can be characterized as hybrid ones, combining continuous and discrete behaviours that are closely related. Changes in the continuous dynamics are usually fired by internal or external ...
详细信息
ISBN:
(纸本)9783030452599;9783030452605
Nowadays, many critical systems can be characterized as hybrid ones, combining continuous and discrete behaviours that are closely related. Changes in the continuous dynamics are usually fired by internal or external discrete events. Due to their inherent complexity, it is a crucial but not trivial task to ensure that these systems satisfy some desirable properties. An approach to analyze them consists of the combination of model-based testing and run-time verification techniques. In this paper, we present an interval logic to specify properties of event-driven hybrid systems and an automatic transformation of the logic formulae into networks of finite-state machines. Currently, we use PROMELA/SPIN to implement the network of finite-state machines, and analyze non-functional properties of mobile applications. We use the TRIANGLE testbed, which implements a controllable network environment for testing, to obtain the application traces and monitor network parameters.
Many transformation techniques developed for constraint logicprograms, also known as constrained Horn clauses (CHCs), have found new useful applications in the field of program verification. In this paper, we work ou...
详细信息
the first-order theory of finite and infinite trees has been studied since the eighties, especially by the logicprogramming community. Following Djelloul, Dao and Frühwirth, we consider an extension of this theo...
详细信息
the proceedings contain 11 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Multivariant Assertion-based Guidance in Abstract Interpretation;guid...
ISBN:
(纸本)9783030138370
the proceedings contain 11 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Multivariant Assertion-based Guidance in Abstract Interpretation;guided Unfoldings for Finding Loops in Standard Term Rewriting;homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms;multiparty Classical Choreographies;a Pragmatic, Scalable Approach to Correct-by-Construction Process Composition Using Classical Linear logic Inference;Confluence of CHR Revisited: Invariants and Modulo Equivalence;compiling Control as Offline Partial Deduction;predicate Specialization for Definitional Higher-Order logicprograms;an Assertion Language for Slicing Constraint logic Languages.
Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always producing useful results. Automatic t...
详细信息
ISBN:
(纸本)9783030138387;9783030138370
Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always producing useful results. Automatic techniques have been studied to prevent precision loss, typically at the expense of larger resource consumption. In both cases (i.e., when analysis produces inaccurate results and when resource consumption is too high), it is necessary to have some means for users to provide information to guide analysis and thus improve precision and/or performance. We present techniques for supporting within an abstract interpretation framework a rich set of assertions that can deal with multivariance/context-sensitivity, and can handle different run-time semantics for those assertions that cannot be discharged at compile time. We show how the proposed approach can be applied to both improving precision and accelerating analysis. We also provide some formal results on the effects of such assertions on the analysis results.
the proceedings contain 33 papers. the topics discussed include: transition systems as method of designing applications in GPGPU technology;context term calculus for rewriting systems;system aspects of design guarante...
the proceedings contain 33 papers. the topics discussed include: transition systems as method of designing applications in GPGPU technology;context term calculus for rewriting systems;system aspects of design guarantee-based cloud calculations;extension of the programsynthesis system to analyze large data sets;equivalence of two parallel execution systems;architecture of software system for hierarchical fuzzy inference;interactive method for cumulative analysis of software formal models behavior;formal foundations for software model to model transformation operation;and ontological similar systems for analysis of texts of natural language.
暂无评论