Search

The existence of a unique solution for a third-order boundary value problem with integral condition is proved in several ways. The main tools in the proofs are the Banach fixed point theorem and the Rus’s fixed point theorem. To compare the applicability of the obtained results, some examples are considered.

Memory allocation and deallocation are the fundamental operations of embedded operating systems, which have been extensively used in many safety critical systems. The correctness of the operations is of paramount importance because their failure could incur severe consequences. While the system is running, the memory state can easily grow to a gigantic amount, which means that it is impossible to verify the huge memory states one by one. Therefore, it is a challenge how to verify the correctness of running memory state of the system. In this article, we propose a novel memory state verification method based on inductive and deductive reasoning. First, we abstract the memory state as a list of memory blocks, which will transform in memory operations. Second, we construct the generic model based on the transition function of the memory management and summarize the invariant properties of the memory state. Third, we use the inductive method to calculate the changes between the memory states, and verify that the memory state of the system always satisfy the global properties. All the proofs are implemented in the interactive theorem prover Coq. On the basis of our proposed model, we verify the correctness of a two-level segregated fit (TLSF) algorithm through some extensions, and we also apply this method to verify the correctness of the memory state of the embedded system at runtime.

This paper presents a solution to the leaderless consensus of multiple spacecraft on SO(3) under a connected undirected graph. An algorithm is proposed to generate an undirected tree graph from a connected undirected communication topology. A distributed observer is designed to estimate the desired attitude and angular velocity for each spacecraft under the generated tree graph. An adaptive controller with a general connected undirected graph is developed to complete the synchronization task. Cases with zero and nonzero final angular velocities are considered. Theoretical proofs and numerical simulations are presented to demonstrate the effectiveness of the proposed controllers.

Sufficient conditions on a smooth, real-valued function g for the nowhere differentiability of $$g\circ p$$ are given, where p is Peano’s curve. This generalizes Sagan’s analytic proof on the nowhere differentiability of the coordinate functions of p. Most of the proofs are geometrically intuitive. The interest about the composites $$g\circ p$$ stems from their recent applications in technical branches.

The minimum-variance portfolio (MVP) has become an essential part of modern portfolio theory, largely due to the availability of its analytical formula and its good out-of-sample performance. When extra constraints such as the long-only constraints are added, MVP in general does not admit an analytical formula anymore. An exceptional case is when the single-factor model holds among the securities considered. It is known that there exists a semi-closed form formula, which relies on an unknown quantity called the long-only beta threshold ( β L ). This note conducts a detailed study of β L and establishes its optimality property that it is the smallest among all possible thresholds. We also develop a simple bisection method for computing β L . Finally we include a mathematical proof for this semi-closed form formula. The results reported provide a deep understanding how the long-only MVP are constructed.

In this paper, we shall give another proof of the faithfulness of Blass translation (for short, B-translation) of the propositional fragment $$\mathbf{L}_1$$ of Leśniewski’s ontology in the modal logic $$\mathbf{K}$$ by means of Hintikka formula. And we extend the result to von Wright-type deontic logics, i.e., ten Smiley-Hanson systems of monadic deontic logic. As a result of observing the proofs we shall give general theorems on the faithfulness of B-translation with respect to normal modal logics complete to certain sets of well-known accessibility relations with a restriction that transitivity and symmetry are not set at the same time. As an application of the theorems, for example, B-translation is faithful for the provability logic $$\mathbf{PrL}$$ (= $$\mathbf{GL}$$ ), that is, $$\mathbf{K}$$ $$+$$ $$\Box (\Box \phi \supset \phi ) \supset \Box \phi $$ . The faithfulness also holds for normal modal logics, e.g., $$\mathbf{KD}$$ , $$\mathbf{K4}$$ , $$\mathbf{KD4}$$ , $$\mathbf{KB}$$ . We shall conclude this paper with the section of some open problems and conjectures.

In this paper we treat metasequents—objects which stand to sequents as sequents stand to formulas—as first class logical citizens. To this end we provide a metasequent calculus, a sequent calculus which allows us to directly manipulate metasequents. We show that the various metasequent calculi we consider are sound and complete w.r.t. appropriate classes of tetravaluations where validity is understood locally. Finally we use our metasequent calculus to give direct syntactic proofs of various collapse results, closing a problem left open in French (Ergo, 3(5), 113–131 2016).

The main purpose of this paper is to generalize the study of the Hecke-Rogers type series, which are the extensions of truncated theorems obtained by Andrews, Merca, Wang and Yee. Our proofs rely heavily on the theory of Bailey pairs.

Proving and refuting are fundamental aspects of mathematical practice that are intertwined in mathematical activity in which conjectures and proofs are often produced and improved through the back-and-forth transition between attempts to prove and disprove. One aspect underexplored in the education literature is the connection between this activity and the construction by students of knowledge, such as mathematical concepts and theorems, that is new to them. This issue is significant to seeking a better integration of mathematical practice and content, emphasised in curricula in several countries. In this paper, we address this issue by exploring how students generate mathematical knowledge through discovering and handling refutations. We first explicate a model depicting the generation of mathematical knowledge throughheuristic refutation(revising conjectures/proofs through discovering and addressing counterexamples) and draw on a model representing different types of abductive reasoning. We employed both models, together with the literature on the teachers’ role in orchestrating whole-class discussion, to analyse a series of classroom lessons involving secondary school students (aged 14–15 years, Grade 9). Our analysis uncovers the process by which the students discovered a counterexample invalidating their proof and then worked via creative abduction where a certain theorem was produced to cope with the counterexample. The paper highlights the roles played by the teacher in supporting the students’ work and the importance of careful task design. One implication is better insight into the form of activity in which students learn mathematical content while engaging in mathematical practice.

We consider batched bin packing. Items are presented in a constant number of batches, and each batch should be packed before the next batch is presented. The cases of two, three, and four batches are studied. We prove improved lower bounds for the standard and parametric variants in some of the cases, and shorten the proofs for all other cases. To achieve this, we apply a new technique in our analysis, which differs from the ones previously used for proving such results.

The calculus of Dependent Object Types (DOT) has enabled a more principled and robust implementation of Scala, but its support for type-level computation has proven insufficient. As a remedy, we propose F ·· ω , a rigorous theoretical foundation for Scala’s higher-kinded types. F ·· ω extends F ω with interval kinds , which afford a unified treatment of important type- and kind-level abstraction mechanisms found in Scala, such as bounded quantification, bounded operator abstractions, translucent type definitions and first-class subtyping constraints. The result is a flexible and general theory of higher-order subtyping. We prove type and kind safety of F ·· ω , as well as weak normalization of types and undecidability of subtyping. All our proofs are mechanized in Agda using a fully syntactic approach based on hereditary substitution.

Formal languages are usually defined in terms of set theory. Choosing type theory instead gives us languages as type-level predicates over strings. Applying a language to a string yields a type whose elements are language membership proofs describing how a string parses in the language. The usual building blocks of languages (including union, concatenation, and Kleene closure) have precise and compelling specifications uncomplicated by operational strategies and are easily generalized to a few general domain-transforming and codomain-transforming operations on predicates. A simple characterization of languages (and indeed functions from lists to any type) captures the essential idea behind language “differentiation” as used for recognizing languages, leading to a collection of lemmas about type-level predicates. These lemmas are the heart of two dual parsing implementations—using (inductive) regular expressions and (coinductive) tries—each containing the same code but in dual arrangements (with representation and primitive operations trading places). The regular expression version corresponds to symbolic differentiation, while the trie version corresponds to automatic differentiation. The relatively easy-to-prove properties of type-level languages transfer almost effortlessly to the decidable implementations. In particular, despite the inductive and coinductive nature of regular expressions and tries respectively, we need neither inductive nor coinductive/bisimulation arguments to prove algebraic properties.

Hodes (2021) “looked under the hood” of the familiar versions of the classical propositional modal logic K and its intuitionistic counterpart (see Plotkin & Sterling 1986). This paper continues that project, addressing some familiar classical strengthenings of K (D, T, K4, KB, K5, Dio (the Diodorian strengthening of K) and GL), and their intuitionistic counterparts (see Plotkin & Sterling 1986 for some of these counterparts). Section 9 associates two intuitionistic one-step proof-theoretic systems to each of the just mentioned intuitionistic logics, this by adding for each a new rule to those which generated IK in Hodes (2021). For the systems associated with the intuitionistic counterparts of D and T, these rules are “pure one-step”: their schematic formulations does not use □ or ♢. For the systems associated with the intuitionistic counterparts of K4, etc., these rules meet these conditions: neither □ nor ♢ is iterated; none use both □ and ♢. The join of the two systems associated with each of these familiar logics is the full one-step system for that intuitionistic logic. And further “blended” intuitionistic systems arise from joining these systems in various ways. Adding the 0-version of Excluded Middle to their intuitionistic counterparts yields the one-step systems corresponding to the familiar classical logics. Each proof-theoretic system defines a consequence relation in the obvious way. Section 10 examines inclusions between these consequence relations. Section 11 associates each of the above consequence relations with an appropriate class of models, and proves them sound with respect to their appropriate class. This allows proofs of some failures of inclusion between consequence relations. (Sections 10 and 11 provide an exhaustive study of a variety of intuitionistic modal logics.) Section 12 proves that the each consequence relation is complete or (for those corresponding to GL) weakly complete, that relative to its appropriate class of models. The Appendix presents three further results about some of the intuitionistic consequence relations discussed in the body of the paper.

In recent years, a number of cryptographic etiquettes have been mechanically verified using a selection of inductive methods. These attestations typically want central a figure of recursive sets of messages, and need deep intuition into why the etiquette is correct. As a result, these proofs frequently require days to weeks of expert effort. We ensure advanced an involuntary verifier, which seems to overawe these glitches for many cryptographic protocols. The code of behavior text to concept a number of first-order invariant the proof commitments mitigating these invariants, along with any user-specified protocol properties are showed from the invariants with a tenacity theorem proved. The individual litheness in construction these invariants is to guesstimate, for each type of nonce and encryption engendered by the protocol, a formulary arresting conditions compulsory for that nonce encryption to be published.

We apply geometric tools to study dynamics of two- and threepeakon solutions of the Camassa–Holm equation. New proofs of asymptotic behavior of the solutions are given. In particular we recover well-known collision conditions. Additionally the Gauss curvature (in the twopeakon case) and the sectional curvature (in the threepeakon case) of corresponding manifolds are computed.

We prove Ibukiyama’s conjectures on Siegel modular forms of half-integral weight and of degree 2 by using Arthur’s multiplicity formula on the split odd special orthogonal group $${\text {SO}}_5$$ and Gan–Ichino’s multiplicity formula on the metaplectic group $${\text {Mp}}_4$$ . In the proof, the representation theory of the Jacobi groups also plays an important role.

This paper is a historical account of the chords theorem, for conic sections from Apollonius to Boscovich. We comment the most significant proofs and applications, focusing on Newton's solution of the Pappus four lines problem. Newton's geometrical achievements drew L'Hospital's attention to the chords theorem as a fundamental one, and led him to search for a simple and direct proof, that he finally obtained by the method of projection. Stirling gave a very elegant algebraic proof; then Boscovich succeeded in finding an almost immediate geometrical proof, and showed how to develop the elements of conic sections starting from this theorem.

Hempel seems to hold the following three views: (H1) Understanding is pragmatic/relativistic: Whether one understands why X happened in terms of Explanation E depends on one's beliefs and cognitive abilities; (H2) Whether a scientific explanation is good, just like whether a mathematical proof is good, is a nonpragmatic and objective issue independent of the beliefs or cognitive abilities of individuals; (H3) The goal of scientific explanation is understanding: A good scientific explanation is the one that provides understanding. Apparently, H1, H2, and H3 cannot be all true. Some philosophers think that Hempel is inconsistent, while some others claim that Hempel does not actually hold H3. I argue that Hempel does hold H3 and that he can consistently hold all of H1, H2, and H3 if he endorses what I call the “understanding argument.” I also show how attributing the understanding argument to Hempel can make more sense of his D-N model and his philosophical analysis of the pragmatic aspects of scientific explanation.

The collective marking strategy with alternative refinement-indicators in adaptive mesh-refining of least-squares finite element methods (LSFEMs) has recently been shown to lead to optimal convergence rates in Carstensen (2020). The proofs utilize explicit identities for the lowest-order Raviart–Thomas and the Crouzeix–Raviart finite elements. This paper generalizes those results to arbitrary polynomial degree and mixed boundary conditions with some novel arguments. The analysis is outlined for the Poisson equation in 3D with mixed boundary conditions.

We consider an algebraic theory with a maximal mass (modified Dirac theory with a $$\gamma_5$$ -expansion of mass). We consider properties of spinors and give the necessary proofs. Quantization is performed.

We study mapping class groups of infinite type surfaces with isolated punctures and their actions on the loop graphs introduced by Bavard-Walker. We classify all of the mapping classes in these actions which are loxodromic with a WWPD action on the corresponding loop graph. The WWPD property is a weakening of Bestvina-Fujiwara's weak proper discontinuity and is useful for constructing non-trivial quasimorphisms. We use this classification to give a sufficient criterion for subgroups of big mapping class groups to have infinite-dimensional second bounded cohomology and use this criterion to give simple proofs that certain natural subgroups of big mapping class groups have infinite-dimensional second bounded cohomology., Final version to appear in Groups, Geometry, and Dynamics

Human-centered automated proof search aims to capture structures of ordinary mathematical proofs and discover human strategies that are used (implicitly) in their construction. We analyze the ways of two theorem provers for approaching that goal. One, the GG the other, Sieg’s AProS system, is described in Sieg and Walsh (Rev Symb Logic 1-35, 2019). Both systems make explicit, via their underlying logical calculi, the goal-directedness and bi-directionality of proof construction. However, the calculus for the GG AProS is to yield humanly intelligible formal proofs by logically and mathematically motivated strategies. In our final Programmatic remarks, we sketch a plausible, but difficult project for achieving more fully G&G’s broad goals by radically separating proof search from proof translation: one could use AProS for the proof search and then exploit the strategic structure of the completed proof as the deterministic underpinning for its translation into a natural language.

This paper is devoted to the study of the motion of a platform maintained on an aircraft in a predetermined position by a system of gyroscopes, which does follows oscillations of the aircraft. Such systems are used for determining the angular position of the aircraft. We briefly review key results on this issue without detailed proofs.

It is widely recognized that students encounter difficulties with proof across all grades and beyond, yet standardized instruments related specifically to students’ perceived self-efficacy for mathematical proof have not been readily available. The purpose of this study was to develop and investigate preliminary validity evidence for a new instrument for measuring self-efficacy for mathematical proof that can be of importance to the field. The new Perceived Self-Efficacy for Proof (PSEP) questionnaire is a self-administered, 8-item questionnaire that quantifies experimentation, conjecturing, inductive reasoning, justification, and validation. To validate the PSEP, two studies with 260 eleventh grade students—recruited from three Dinaledi schools in EThekwini metropolitan area, South Africa—were conducted. In Study 1 (n=128), face and content validity were evaluated, and an exploratory factor analysis (EFA) was performed. In Study 2 (n=132), a confirmatory factor analysis (CFA) was conducted and external validity was investigated. In both samples, the PSEP was found to possess good internal consistency reliability with relatively high factor loadings on a single component. Although the findings in this report represent preliminary validation evidence, it can be concluded that the PSEP is a valid, reliable and sensitive measure of 11th grade students’ perceptions of their ability to construct a proof and may serve as a meaningful outcome in mathematical proof research and classroom proof education.

We consider the K -interpolation methods involving slowly varying functions. We establish some reiteration formulae including so-called L or R limiting interpolation spaces as well as the R R , R L , L R , and L L extremal interpolation spaces. These spaces arise in the limiting situations. The proofs of most reiteration formulae are based on Holmstedt-type formulae. Applications to grand and small Lorentz spaces in critical cases are given.

We formalize several regular numeral systems, state their properties and supported operations, clarify the correctness, and tabulate the proofs. Our goal is to use as few symbols in the presentation of digits and make as few digit changes as possible in every operation. Most importantly, we introduce two new systems: (1) the buffered regular system is simple and allows the increment and decrement of the least-significant digit in constant time, and (2) the strictly regular system allows the increment and decrement of a digit at arbitrary position with a constant number of digit changes while using three symbols only (instead of four symbols required by the extended regular system). To demonstrate the usefulness of the regular systems, we survey how they have been used in the design of data structures.

This paper presents HashWires, a hash-based range proof protocol that is applicable in settings for which there is a trusted third party (typically a credential issuer) that can generate commitments. We refer to these as “credential-based” range proofs (CBRPs). HashWires improves upon hashchain solutions that are typically restricted to micro-payments for small interval ranges, achieving an exponential speedup in proof generation and verification time. Under reasonable assumptions and performance considerations, a Hash-Wires proof can be as small as 305 bytes for 64-bit integers. Although CBRPs are not zero-knowledge and are inherently less flexible than general zero-knowledge range proofs, we provide a number of applications in which a credential issuer can leverage HashWires to provide range proofs for private values, without having to rely on heavyweight cryptographic tools and assumptions.

PurposeThe purpose of this article is to derive formulas for lifetime expected credit loss of loans that are required for the calculation of loan loss reserves under IFRS 9. This is done both for fixed-rate and floating rate loans under different assumptions on LGD modeling, prepayment, and discount rates.Design/methodology/approachThis study provides exact formulas for lifetime expected credit loss derived analytically together with the mathematical proofs of each expression.FindingsThis articles shows that the formula most commonly applied in the literature for calculating lifetime expected credit loss is inconsistent with measuring expected loss based on expected discounted cash flows. Formulas based on discounted cash flows always lead to more conservative numbers.Practical implicationsFor banks reporting under IFRS 9, the implication of this research is a better understanding of the different approaches used for computing lifetime expected loss, how they are connected, and what assumptions are underlying each approach. This may lead to corrections in existing frameworks to make applications of risk management systems more consistent.Originality/valueWhile there is a lot of literature explaining IFRS 9 and evaluating its impact, none of the existing research has systematically analyzed the calculation of lifetime expected credit loss for this purpose and how the formula changes under different modeling assumptions. This gap is filled by this study.

Recently the first author proved a congruence proposed in 2006 by Adamchuk: [Formula: see text] for any prime [Formula: see text]. In this paper, we provide more examples (with proofs) of congruences of the same kind [Formula: see text] where [Formula: see text] is a prime such that [Formula: see text], [Formula: see text] is a fraction in [Formula: see text] and [Formula: see text] is a [Formula: see text]-adic integer. The key ingredients are the [Formula: see text]-adic Gamma function [Formula: see text] and a special class of computer-discovered hypergeometric identities.

In traditional mathematics lectures the instructor normally writes the definitions, theorems, and proofs covered on the board, and gives informal oral explanations that help to make sense of them. The students have to take notes. However, there are serious problems concerning students’ note-taking in traditional mathematics lectures. Students often cannot think about the information presented during the lecture as they are busy writing. Making sense of the content later is also difficult because many students do not include the lecturer’s oral explanations in their notes. One approach to addressing these problems can be the use of guided notes: a modified version of the instructor’s notes with certain blanks the students have to fill in during the lecture. We investigated to what extent guided notes can support students in their note-taking in mathematics lectures in a study using a mixed-method design. This study provides on the one hand quantitative data suggesting that guided notes are perceived as beneficial by many students for several aspects of their note-taking. On the other hand, it offers qualitative data illustrating how the use of guided notes can influence these aspects. The results indicate in particular that the use of guided notes can address some of the problems concerning students’ note-taking in traditional mathematics lectures, while it can also lead to new problems that one needs to be aware of.

The problem of finding, among the Euler parallelepipeds, one with an integer spatial diagonal, called the perfect cuboid problem, is one of the unsolved mathematical problems from the section of number theory. This article provides mathematical proof of the impossibility of the existence of the perfect cuboide among all possible Euler parallelepipeds. A mathematical justification for an equivalence of the problem of doubling a cube and the problem of constructing a perfect cuboid is also given.

Formal verification is to use mathematical methods to prove that our scheme is correct. This scheme is just a pronoun. It may be expressed as a hardware, a software or an algorithm. Errors in hardware are more difficult to modify than errors in software, so formal proofs and inspections often appear in the argument for hardware design. But, it does not mean that the software does not need to be formally verified. In addition to digital circuits or combinational circuits, cryptographic protocols also need to be formally verified. Formal proof can only ensure whether the result of logical inference is consistent with the previous stage, and can not guarantee whether there are defects in the process of logical inference. In this article the authors take as an example of Zhang-Wang's digital signature algorithm, and point out two formal proof methods of Boolean algebra and Galois field respectively.

This exploratory study reports on characteristics of proof production and proof writing observed in the work of first-year university students who took part in workshops on the theorem prover LEAN (https://leanprover.github.io). These workshops were voluntary and offered alongside a transition to proof module in a UK university. Through qualitative analysis of 36 student produced proofs of an unfamiliar statement we highlight characteristics of proofs produced by students who did engaged and who did not engage with LEAN. The analysis shows two characteristics of proofs written by students who engaged with the programming language. The first concerns proof writing and includes the accurate and correct use of mathematics language and symbols, together with the use of complete sentences and punctuations in proofs. The second concerns proof structure and includes the overt break down of proofs in goals and sub-goals. We conclude by hypothesising a link between the characteristics observed and the experience of engaging with the theorem prover and we reflect on the potential that engagement with this theorem prover may have in mathematics instruction at university level.

International audience; We present results of existence, regularity and uniqueness of solutions of the master equation associated with the mean field planning problem in the finite state space case, in the presence of a common noise. The results hold under monotonicity assumptions, which are used crucially in the different proofs of the paper. We also make a link with the trajectories induced by the solution of the master equation and start a discussion on the case of boundary conditions.

This brief investigates consensus of multi-agent systems via asynchronous impulsive control. Firstly, the model considered in this brief accords with actual situation. Secondly, a new control scheme is proposed, which not only can greatly reduce communication and control cost, but also effectively solves the problem of excessive power. Moreover, sufficient conditions formulated by linear matrix inequalities are developed to obtain the less conservative results. The consensus error bound and the convergence rate are also given by rigorous mathematical proof. Finally, a numerical simulation is given to verify the theoretical analysis.

On the basis of the analysis of the functioning of complex special-purpose information systems, a general approach was proposed to their mathematical modeling and structural decomposition, based on topological constructions using the theory of the final semigroups. The connection between any transformations of a complex system in the finite space of its states and certain valid coordinatization variants is defined for the final semigroups. Various generalized indicators of evaluation of functional structure simplexes, which allowed one to obtain the characteristics of these complexes, have been determined. The proposed method of analysis allowed more objective analysis of the q-connectivity of the simplexes and the observability and controllability of the special-purpose complex information system. Definitions, theorems, and proofs are presented, which allows calculation of the sequence of composition and the integration of the subsystems of a complex system into a single whole.

In this paper we exploit elementary combinatorial techniques to settle different cryptanalytic observations on RC4 that remained unproved for more than two decades. At the same time, we present new observations with theoretical proofs. We first prove the biases (non-randomness) presented by Fluhrer and McGrew (FSE 2000) two decades ago. It is surprising that though the biases have been published long back, and there are many applications of them in cryptanalysis till recent days as well, the proofs have never been presented. In this paper, we complete that task and also show that any such bias immediately provides a glimpse of hidden variables in RC4. Further, we take up the biases of two non-consecutive key-stream bytes skipping one byte in between. We show the incompleteness of such a result presented by SenGupta et al. (JoC, 2013) and provide new observations and proofs in this direction relating the key-stream bytes and glimpses. Similarly, we streamline certain missed observation in the famous Glimpse theorem presented by Jenkins in 1996. Our results point out how biases of RC4 key-stream and the Glimpses of the RC4 hidden variables are related. It is evident from our results that the biases and glimpses are everywhere in RC4 and it needs further investigation as we provide very high magnitude of glimpses that were not known earlier.

Class imbalance is one of the most popular and important issues in the domain of classification. The AdaBoost algorithm is an effective solution for classification, but it still needs improvement in the imbalanced data problem. This paper proposes a method to improve the AdaBoost algorithm using the new weighted vote parameters for the weak classifiers. Our proposed weighted vote parameters are determined not only by the global error rate but also by the classification accuracy rate of the positive class, which is our primary interest. The imbalanced index of the data is also a factor in constructing our algorithms. Our proposed algorithms outperform the traditional ones, especially regarding the evaluation criterion of F - 1 Measure . Theoretic proofs of the advantages of our proposed algorithms are presented. Two kinds of simulated datasets and four real datasets are applied in the experiment as the specific support to our proposed algorithms.

In the present work, we consider Zuckerberg's method for geometric convex-hull proofs introduced in [Geometric proofs for convex hull defining formulations, Operations Research Letters 44(5), 625-629 (2016)]. It has only been scarcely adopted in the literature so far, despite the great flexibility in designing algorithmic proofs for the completeness of polyhedral descriptions that it offers. We suspect that this is partly due to the rather heavy algebraic framework its original statement entails. This is why we present a much more lightweight and accessible approach to Zuckerberg's proof technique, building on ideas from [Extended formulations for convex hulls of some bilinear functions, Discrete Optimization 36, 100569 (2020)]. We introduce the concept of set characterizations to replace the set-theoretic expressions needed in the original version and to facilitate the construction of algorithmic proof schemes. Along with this, we develop several different strategies to conduct Zuckerberg-type convex-hull proofs. Very importantly, we also show that our concept allows for a significant extension of Zuckerberg's proof technique. While the original method was only applicable to 0/1-polytopes, our extended framework allows to treat arbitrary polyhedra and even general convex sets. We demonstrate this increase in expressive power by characterizing the convex hull of Boolean and bilinear functions over polytopal domains. All results are illustrated with indicative examples to underline the practical usefulness and wide applicability of our framework.