We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory S12 proves the consistency of PETS. Our approach employs models for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.

journalknowledge tech

Robotics and Computer-Integrated Manufacturing (2022), 74, 102281

Publication year: 2022

In the context of Industry 4.0, smart factories use advanced sensing and data analytic technologies to understand and monitor the manufacturing processes. To enhance production efficiency and reliability, statistical Artificial Intelligence (AI) technologies such as machine learning and data mining are used to detect and predict potential anomalies within manufacturing processes. However, due to the heterogeneous nature of industrial data, sometimes the knowledge extracted from industrial data is presented in a complex structure. This brings the semantic gap issue which stands for the lack of interoperability among different manufacturing systems. Furthermore, as the Cyber-Physical Systems (CPS) are becoming more knowledge-intensive, uniform knowledge representation of physical resources and real-time reasoning capabilities for analytic tasks are needed to automate the decision- making processes for these systems. These requirements highlight the potential of using symbolic AI for predictive maintenance.

To automate and facilitate predictive analytics in Industry 4.0, in this paper, we present a novel Knowledge-based System for Predictive Maintenance in Industry 4.0 (KSPMI). KSPMI is developed based on a novel hybrid approach that leverages both statistical and symbolic AI technologies. The hybrid approach involves using statistical AI technologies such as machine learning and chronicle mining (a special type of sequential pattern mining approach) to extract machine degradation models from industrial data. On the other hand, symbolic AI technologies, especially domain ontologies and logic rules, will use the extracted chronicle patterns to query and reason on system input data with rich domain and contextual knowledge. This hybrid approach uses Semantic Web Rule Language (SWRL) rules generated from chronicle patterns together with domain ontologies to perform ontology reasoning, which enables the automatic detection of machinery anomalies and the prediction of future events’ occurrence. KSPMI is evaluated and tested on both real-world and synthetic data sets.

Following the trend of Industry 4.0, the business model of steel manufacturing is transforming from a historical inwardly focused supplier/customer relationship to one that embraces the wider end-to-end supply chain and improves productivity more holistically. However, the data and information required for supply chain planning and steelmaking process modelling are normally distributed over scattered sources across organisation boundaries and research communities. This leads to a major problem concerning semantic interoperability. To address this issue, this paper introduces a Com- mon Reference Ontology for Steelmaking (CROS). CROS serves as a shared steelmaking resource and capability model that aims to facilitate knowledge modelling, knowledge sharing and information management. In contrast to most of the existing steelmaking ontologies which merely focus on conceptual modelling, our work pays special attention to the real-world implementation and utilisation aspects of CROS. The functionality and usefulness of CROS is evaluated and tested on a real-world condition-based monitoring and maintenance task for cold rolling mills at Tata Steel in the United Kingdom.

This paper introduces the Steel Cold Rolling Ontology (SCRO) to model and capture domain knowledge of cold rolling processes and activities within a steel plant. A case study is set up that uses real-world cold rolling data sets to validate the performance and functionality of SCRO. This includes using the Ontop framework to deploy virtual knowledge graphs for data access, data integration, data querying, and condition-based maintenance purposes. SCRO is evaluated using OOPS!, the ontology pitfall detection system, and feedback from domain experts from Tata Steel.

Cyber Physical Trust Systems (CPTS) are Cyber Physical Systems and Internet of Things enriched with trust as an explicit, measurable, testable and verifiable system component. In this paper, we propose to use blockchain, a distributed ledger technology, as the trust enabling system component for CPTS. We propose two schemes for CPTSs driven by blockchain in relation to two typical network model cases. We show that our proposed approach achieves the security properties, such as device identification, authentication, integrity, and non-repudiation, and provides protection against popular attacks, such as replay and spoofing. We provide formal proofs of those properties using the Tamarin Prover tool. We describe results of a proof-of-concept which implements a CPTS driven by blockchain for physical asset management and present a performance analysis of our implementation. We identify use cases in which CPTSs driven by blockchain find applications.

journal

Annals of Pure and Applied Logic, Volume 170, Issue 10, pp. 1176-1187

Publication year: 2019

This paper studies the complexity of constant depth propositional proofs in the cedent and sequent calculus. We discuss the relationships between the size of tree-like proofs, the size of dag-like proofs, and the heights of proofs. The main result is to correct a proof construction in an earlier paper about transformations from proofs with polylogarithmic height and constantly many formulas per cedent.

journal

Journal Logic Computation, Volume 28, Issue 6, September 2018, Pages 1125–1187.

Publication year: 2018

We introduce a system of Hyper Natural Deduction for Gödel Logic as an extension of Gentzen’s system of Natural Deduction. A deduction in this system consists of a finite set of derivations which uses the typical rules of Natural Deduction, plus additional rules providing means for communication between derivations. We show that our system is sound and complete for infinite-valued propositional Gödel Logic, by giving translations to and from Avron’s Hypersequent Calculus. We provide conversions for normalization extending usual conversions for Natural Deduction and prove the existence of normal forms for Hyper Natural Deduction for Gödel Logic. We show that normal deductions satisfy the subformula property.

The Cobham Recursive Set Functions (CRSF) provide an analogue of polynomial time computation which applies to arbitrary sets. We give three new equivalent characterizations of CRSF. The first is algebraic, using subset-bounded recursion and a form of Mostowski collapse. The second is our main result: the CRSF functions are shown to be precisely the functions computed by a class of uniform, infinitary, Boolean circuits. The third is in terms of a simple extension of the rudimentary functions by transitive closure and subset-bounded recursion.

We study consistency search problems for Frege and extended Frege proofs, namely the NP search problems of finding syntactic errors in Frege and extended Frege proofs of contradictions. The input is a polynomial time function, or an oracle, describing a proof of a contradiction; the output is the location of a syntactic error in the proof. The consistency search problems for Frege and extended Frege systems are shown to be many-one complete for the provably total NP search problems of the second order bounded arithmetic theories U^1_2 and V^1_2 , respectively.

We show that logics based on linear Kripke frames – with or without constant domains – that have a scattered end piece are not recursively enumerable. This is done by reduction to validity in all finite classical models.

feasible set fctsjournal

Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore: Volume 33, 2017, pp. 55-116

Publication year: 2017

This paper introduces bounded fragments of Kripke Platek set theory which characterise the *Cobham Recursive Set Functions.*

This paper introduces the *Cobham Recursive Set Functions* (CRSF) as a version of polynomial time computable functions on general sets, based on a limited (bounded) form of epsilon-recursion. This is inspired by Cobham’s classic definition of polynomial time functions based on limited recursion on notation. We introduce a new set composition function, and a new smash function for sets which allows polynomial increases in the ranks and in the cardinalities of transitive closures. We bootstrap CRSF, prove closure under (unbounded) replacement, and prove that any CRSF function is embeddable into a smash term. When restricted to natural encodings of binary strings as hereditarily finite sets, the CRSF functions define precisely the polynomial time computable functions on binary strings. Prior work of Beckmann, Buss and Friedman and of Arai introduced set functions based on safe-normal recursion in the sense of Bellantoni-Cook. We prove an equivalence between our class CRSF and a variant of Arai’s predicatively computable set functions.

We consider intermediate predicate logics defined by fixed well-ordered (or dually well-ordered) linear Kripke frames with constant domains where the order-type of the well-order is strictly smaller than~$\omega^\omega$. We show that two such logics of different order-type are separated by a first-order sentence using only one monadic predicate symbol. Previous results by Minari, Takano and Ono, as well as the second author, obtained the same separation but relied on the use of predicate symbols of unbounded arity.

We introduce the *safe recursive set functions* based on a Bellantoni-Cook style subclass of the primitive recursive set functions. We show that the functions computed by safe recursive set functions under a list encoding of finite strings by hereditarily finite sets are exactly the polynomial growth rate functions computed by alternating exponential time Turing machines with polynomially many alternations. We also show that the functions computed by safe recursive set functions under a more efficient binary tree encoding of finite strings by hereditarily finite sets are exactly the quasipolynomial growth rate functions computed by alternating quasipolynomial time Turing machines with polylogarithmic many alternations.

We characterize the safe recursive set functions on arbitrary sets in definability-theoretic terms. In its strongest form, we show that a function on arbitrary sets is safe recursive if, and only if, it is uniformly definable in some polynomial level of a refinement of Jensen’s J-hierarchy, relativised to the transitive closure of the function’s arguments.

We observe that safe-recursive functions on infinite binary strings are equivalent to functions computed by so-called infinite-time Turing machines in time less than ω^ω. We also give a machine model for safe recursion which is based on set-indexed parallel processors and the natural bound on running times.

A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy.

Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form.

This paper concerns the second order systems U^1_2 and V^1_2 of bounded arithmetic, which have proof theoretic strengths corresponding to polynomial space and exponential time computation. We formulate improved witnessing theorems for these two theories by using S^1_2 as a base theory for proving the correctness of the polynomial space or exponential time witnessing functions. We develop the theory of nondeterministic polynomial space computation in U^1_2 . Kołodziejczyk, Nguyen, and Thapen have introduced local improvement properties to characterize the provably total NP functions of these second order theories. We show that the strengths of their local improvement principles over U^1_2 and V^1_2 depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U^1_2 proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically rounds is complete for the provably total NP search problems of V^1_2 . Related results are obtained for local improvement principles with one improvement round, and for local improvement over rectangular grids.

The paper corrects earlier upper bounds on the size of free-cut elimination. Free-cut elimination allows cut elimination to be carried out in the presence of non-logical axioms. The correction requires that the notion of a free-cut be modified so that a cut formula is anchored provided that all of its introductions are anchored, instead of only requiring that one of its introductions is anchored. With the correction, the originally proved size upper bounds remain unchanged. These results also apply to partial cut elimination. We also apply these bounds to elimination of cuts in propositional logic.

If the non-logical inferences are closed under cut and infer only atomic formulas, then all cuts can be eliminated. This generalizes earlier results of Takeuti and of Negri and van Plato.

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.

journal

In: Ways of Proof Theory, ed. R. Schindler, Ontos Series on Mathematical Logic, pp. 65-134, 2010.

Publication year: 2010

The complexity class of Π^p_k – Polynomial Local Search (PLS) problems with Π^p_l – goal is introduced, and is used to give new characterisations of definable search problems in fragments of Bounded Arithmetic. The characterisations are established via notations for propositional proofs obtained by translating Bounded Arithmetic proofs using the Paris-Wilkie-translation. For l ≤ i ≤ k , the Σ bi – definable search problems of T^k+1_2 are exactly characterised by Π^p_k – PLS problems with Π^p_l – goals. These Π^p_k – PLS problems can be defined in a weak base theory such as S^1_2 , and proved to be total in T^k+1_2 . Furthermore, the Π^p_k – PLS definitions can be Skolemised with simple polynomial time functions. The Skolemised Π^p_k – PLS definitions give rise to a new ∀Σ^b_1(α) – principle conjectured to separate T^k_2(α) and T^k+1_2(α).

The complexity class of Π^p_k – polynomial local search (PLS) problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1 ≤ i ≤ k+1 , the Σ^b_i – definable functions of T^k+1_2 are characterized in terms of Π^p_k – PLS problems. These Π^p_k – PLS problems can be defined in a weak base theory such as S^1_2 , and proved to be total in T^k+1_2 . Furthermore, the Π^p_k – PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. We introduce a new ∀Σ^b_1(α) – principle that is conjectured to separate T^k_2(α) and T^k+1_2(α) .

We investigate the relation of countable closed linear orderings with respect to continuous monotone embeddability and show that there are exactly ℵ1 many equivalence classes with respect to this embeddability relation. This is an extension of Laver’s result, who considered (plain) embeddability, which yields coarser equivalence classes. Using this result we show that there are only ℵ0 many different Gödel logics.

We investigate the relation between logics of countable linear Kripke frames with constant domains and Gödel logics. We show that for any such Kripke frame there is a Gödel logic which coincides with the logic of this Kripke frame and vice versa. This allows us to transfer several recent results on Gödel logics to the logics of countable linear Kripke frames with constant domains.

journal

Logic Colloquium '02, Lecture Notes in Logic 27: 48-74, Association for Symbolic Logic, La Jolla, CA, 2006.

Publication year: 2006

We extend the definition of dynamic ordinals to generalised dynamic ordinals. We compute generalised dynamic ordinals of all fragments of relativised bounded arithmetic by utilising methods from Boolean complexity theory, similar to [Krajicek1994]. We indicate the role of generalised dynamic ordinals as universal measures for implicit computational complexity. I.e., we describe the connections between generalised dynamic ordinals and witness oracle Turing machines for bounded arithmetic theories. In particular, through the determination of generalised dynamic ordinals we re-obtain well-known independence results for relativised bounded arithmetic theories.

We define the notion of the *uniform reduct* of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are Π^0_1-hard and obviously in Σ^0_2. We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true Π^b_1(α)-formulas.

This paper proves exponential separations between depth d-LK and depth (d+1/2)-LK for every d in 0, 1/2, 1, 1 1/2,… utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth (d+1)-LK for d in 0,1,2,… . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for d in 0, 1/2, 1, 1 1/2,… and describe transformations between them.

We define a general method to lift principles requiring exponential tree-size (d+1/2)-LK-refutations for d in 0,1,2,… to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle and d=0. From this we also deduce width lower bounds for resolution refutations of the Ramsey principle.

The theories S^i_1(α) and T^i_1(α) are the analogues of Buss’ relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i , a Σ^b_i+1(α) – formula TOP^i(α), which expresses a form of the total ordering principle, is exhibited that is provable in S^i+1_1(α) , but unprovable in T^i_1(α). This is in contrast with the classical situation, where S^i+1_2 is conservative over T^i_2 w.r.t. Σ^b_i+1-sentences. The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems.

We define and study a new restricted consistency notion for bounded arithmetic theories T2j. It is the strongest ∀Π1b-statement over S21 provable in T2j, similar to Con(Gi) in Krajíček and Pudlák, (Z. Math. Logik Grundl. Math. 36 (1990) 29) or RCon(Ti1) in Krajı́ček and Takeuti (Ann. Math. Artificial Intelligence 6 (1992) 107). The advantage of our notion over the others is that can directly be used to construct models of T2j. We apply this by proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The ∀Π1b-separation of bounded arithmetic theories S2i from T2j (1⩽i⩽j) is equivalent to the existence of a model of S2i which does not have a Δ0b-elementary extension to a model of T2j.

Ordinal notations and provability of well-foundedness have been a central tool in the study of the consistency strength and computational strength of formal theories of arithmetic. This development began with Gentzen’s consistency proof for Peano arithmetic based on the well-foundedness of ordinal notations up to ε_0 . Since the work of Gentzen, ordinal notations and provable well-foundedness have been studied extensively for many other formal systems, some stronger and some weaker than Peano arithmetic. In the present paper, we investigate the provability and non-provability of well-foundedness of ordinal notations in very weak theories of bounded arithmetic, notably the theories S^i_2 and T^i_2 with 1 ≤ i ≤ 2 . We prove several results about the provability of well-foundedness for ordinal notations; our main results state that for the usual ordinal notations for ordinals below ε_0 and Γ_0, the theories T^i2 and S^2_2 can prove the ordinal Σ^b_1 – minimization principle over a bounded domain. PLS is the class of functions computed by a polynomial local search to minimize a cost function. It is a corollary of our theorems that the cost function can be allowed to take on ordinal values below Γ_0 , without increasing the class PLS .

Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of Π^b_1(α) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories Σ^b_n(α)-L^mIND for m=n and m=n+1, n≥0 . Different dynamic ordinals lead to separation. Therefore, we will obtain several separation results between these relativized theories. We will generalize our results to arbitrary languages extending the language of Peano arithmetic.

We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definition of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S^1_2 . In particular this solves an open problem formulated by Takeuti.