Browse
Submit Data
Databases
API
Help

Dataset Information

15 Views

0 Connections

0 Citations

0 Reanalyses

0 Downloads

Omics score: 0

Universal (meta-)logical reasoning: The Wise Men Puzzle (Isabelle/HOL dataset).

ABSTRACT: The authors universal (meta-)logical reasoning approach is demonstrated and assessed with a prominent riddle in epistemic reasoning: the Wise Men Puzzle. The presented solution puts a particular emphasis on the adequate modeling of common knowledge and it illustrates the elegance and the practical relevance of the shallow semantical embedding approach when utilized within modern proof assistant systems such as Isabelle/HOL. The contributed dataset provides supporting evidence for claims made in the article "Universal (meta-)logical reasoning: Recent successes" (Benzmüller, 2019).

SUBMITTER: Benzmuller C

PROVIDER: S-EPMC6468147 | biostudies-literature | 2019 Jun

REPOSITORIES: biostudies-literature

ACCESS DATA

Json Xml

Publications

Universal (meta-)logical reasoning: The Wise Men Puzzle (Isabelle/HOL dataset).

Benzmüller Christoph C

Data in brief 20190320

The authors universal (meta-)logical reasoning approach is demonstrated and assessed with a prominent riddle in epistemic reasoning: the Wise Men Puzzle. The presented solution puts a particular emphasis on the adequate modeling of common knowledge and it illustrates the elegance and the practical relevance of the shallow semantical embedding approach when utilized within modern proof assistant systems such as Isabelle/HOL. The contributed dataset provides supporting evidence for claims made in ...[more]

PMID: 31016212

Similar Datasets

LogiKEy workbench: Deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle/HOL dataset).

Project description:The LogiKEy workbench and dataset for ethical and legal reasoning is presented. This workbench simultaneously supports development, experimentation, assessment and deployment of formal logics and ethical and legal theories at different conceptual layers. More concretely, it comprises, in form of a dataset (Isabelle/HOL theory files), formal encodings of multiple deontic logics, logic combinations, deontic paradoxes and normative theories in the higher-order proof assistant system Isabelle/HOL. The data were acquired through application of the LogiKEy methodology, which supports experimentation with different normative theories, in different application scenarios, and which is not tied to specific logics or logic combinations. Our workbench consolidates related research contributions of the authors and it may serve as a starting point for further studies and experiments in flexible and expressive ethical and legal reasoning. It may also support hands-on teaching of non-trivial logic formalisms in lecture courses and tutorials. The LogiKEy methodology and framework is discussed in more detail in the companion research article titled "Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support" [5].

| S-EPMC7586073 | biostudies-literature

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

Project description:We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle’s code generator. The development combines various existing formalizations such as matrices, Sturm’s theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.

| S-EPMC7089722 | biostudies-literature

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.

Project description:In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximation with the argument principle, we are able to make use of remainder sequences to effectively count the number of complex roots of a polynomial within some domains, such as a rectangular box and a half-plane.

| S-EPMC6995451 | biostudies-literature

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL

Project description:The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number theory, computer algebra and cryptography. In this paper, we provide an implementation of the LLL algorithm. Both its soundness and its polynomial running-time have been verified using Isabelle/HOL. Our implementation is nearly as fast as an implementation in a commercial computer algebra system, and its efficiency can be further increased by connecting it with fast untrusted lattice reduction algorithms and certifying their output. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.

| S-EPMC7413592 | biostudies-literature

Wise reasoning, intergroup positivity, and attitude polarization across contexts.

Project description:We hypothesized that a wisdom-based reasoning process comprised of epistemic humility, accounting for context, and integrating different perspectives and interests, would be helpful in overcoming intergroup bias and attitude polarization in societal conflicts. Here we test the hypothesis using both the Situated Wise Reasoning Scale and experimental induction. In each study, we recruited participants who self-identified as members of a group implicated in an ongoing intergroup situation. In five correlational studies (Studies 1-5) we examined the relations between measured wise reasoning and intergroup positivity and attitude polarization. In two experiments, we tested the effects of a brief online wise-reasoning thought exercise on intergroup positivity and polarization (Studies 6-7), and charitable behaviors to an outgroup (Study 6). We found that wise reasoning relates to more positivity toward outgroups and less attitude polarization across different groups and conflicts. The results have implications for theory and may also have implications for future research on interventions to improve intergroup relations.

| S-EPMC8175723 | biostudies-literature

Role of the Hippocampus During Logical Reasoning and Belief Bias in Aging.

Project description:Reasoning requires initial encoding of the semantic association between premises or assumptions, retrieval of these semantic associations from memory, and recombination of information to draw a logical conclusion. Currently-held beliefs can interfere with the content of the assumptions if not congruent and inhibited. This study aimed to investigate the role of the hippocampus and hippocampal networks during logical reasoning tasks in which the congruence between currently-held beliefs and assumptions varies. Participants of younger and older age completed a series of syllogistic reasoning tasks in which two premises and one conclusion were presented and they were required to decide if the conclusion logically followed the premises. The belief load of premises was manipulated to be either congruent or incongruent with currently-held beliefs. Our whole-brain results showed that older adults recruited the hippocampus during the premise integration stage more than their younger counterparts. Functional connectivity using a hippocampal seed revealed that older, but not younger, adults recruited a hippocampal network that included anterior cingulate and inferior frontal regions when premises were believable. Importantly, this network contributed to better performance in believable inferences, only in older adults group. Further analyses suggested that, in older adults group, the integrity of the left cingulum bundle was associated with the higher rejection of believable premises more than unbelievable ones. Using multimodal imaging, this study highlights the importance of the hippocampus during premise integration and supports compensatory role of the hippocampal network during a logical reasoning task among older adults.

| S-EPMC7232576 | biostudies-literature

Aging effects on discrimination learning, logical reasoning and memory in pet dogs.

Project description:In laboratory dogs, aging leads to a decline in various cognitive domains such as learning, memory and behavioural flexibility. However, much less is known about aging in pet dogs, i.e. dogs that are exposed to different home environments by their caregivers. We used tasks on a touchscreen apparatus to detect differences in various cognitive functions across pet Border Collies aged from 5 months to 13 years. Ninety-five dogs were divided into five age groups and tested in four tasks: (1) underwater photo versus drawing discrimination, (2) clip art picture discrimination, (3) inferential reasoning by exclusion and (4) a memory test with a retention interval of 6 months. The tasks were designed to test three cognitive abilities: visual discrimination learning, logical reasoning and memory. The total number of sessions to reach criterion and the number of correction trials needed in the two discrimination tasks were compared across age groups. The results showed that both measures increased linearly with age, with dogs aged over 13 years displaying slower learning and reduced flexibility in comparison to younger dogs. Inferential reasoning ability increased with age, but less than 10 % of dogs showed patterns of choice consistent with inference by exclusion. No age effect was found in the long-term memory test. In conclusion, the discrimination learning tests used are suitable to detect cognitive aging in pet dogs, which can serve as a basis for comparison to help diagnose cognition-related problems and as a tool to assist with the development of treatments to delay cognitive decline.

| S-EPMC5005891 | biostudies-other

Social class and wise reasoning about interpersonal conflicts across regions, persons and situations.

Project description:We propose that class is inversely related to a propensity for using wise reasoning (recognizing limits of their knowledge, consider world in flux and change, acknowledges and integrate different perspectives) in interpersonal situations, contrary to established class advantage in abstract cognition. Two studies-an online survey from regions differing in economic affluence (n = 2 145) and a representative in-lab study with stratified sampling of adults from working and middle-class backgrounds (n = 299)-tested this proposition, indicating that higher social class consistently related to lower levels of wise reasoning across different levels of analysis, including regional and individual differences, and subjective construal of specific situations. The results held across personal and standardized hypothetical situations, across self-reported and observed wise reasoning, and when controlling for fluid and crystallized cognitive abilities. Consistent with an ecological framework, class differences in wise reasoning were specific to interpersonal (versus societal) conflicts. These findings suggest that higher social class weighs individuals down by providing the ecological constraints that undermine wise reasoning about interpersonal affairs.

| S-EPMC5745406 | biostudies-literature

Implementing a universal gate set on a logical qubit encoded in an oscillator.

Project description:A logical qubit is a two-dimensional subspace of a higher dimensional system, chosen such that it is possible to detect and correct the occurrence of certain errors. Manipulation of the encoded information generally requires arbitrary and precise control over the entire system. Whether based on multiple physical qubits or larger dimensional modes such as oscillators, the individual elements in realistic devices will always have residual interactions, which must be accounted for when designing logical operations. Here we demonstrate a holistic control strategy which exploits accurate knowledge of the Hamiltonian to manipulate a coupled oscillator-transmon system. We use this approach to realize high-fidelity (98.5%, inferred), decoherence-limited operations on a logical qubit encoded in a superconducting cavity resonator using four-component cat states. Our results show the power of applying numerical techniques to control linear oscillators and pave the way for utilizing their large Hilbert space as a resource in quantum information processing.A logical qubit is a two-dimensional subspace of a higher dimensional system, whose manipulation requires precise control over the whole system. Here the authors demonstrate a control strategy which exploits precise knowledge of the Hamiltonian to manipulate a coupled oscillator-transmon system.

| S-EPMC5522494 | biostudies-literature

Universal Chimeric Antigen Receptors for Multiplexed and Logical Control of T Cell Responses.

Project description:T cells expressing chimeric antigen receptors (CARs) are promising cancer therapeutic agents, with the prospect of becoming the ultimate smart cancer therapeutics. To expand the capability of CAR T cells, here, we present a split, universal, and programmable (SUPRA) CAR system that simultaneously encompasses multiple critical "upgrades," such as the ability to switch targets without re-engineering the T cells, finely tune T cell activation strength, and sense and logically respond to multiple antigens. These features are useful to combat relapse, mitigate over-activation, and enhance specificity. We test our SUPRA system against two different tumor models to demonstrate its broad utility and humanize its components to minimize potential immunogenicity concerns. Furthermore, we extend the orthogonal SUPRA CAR system to regulate different T cell subsets independently, demonstrating a dually inducible CAR system. Together, these SUPRA CARs illustrate that multiple advanced logic and control features can be implemented into a single, integrated system.

| S-EPMC5984158 | biostudies-literature

OmicsDI is part of the ELIXIR infrastructure

OmicsDI is an Elixir interoperability service. Learn more ›

OmicsDI Databases

PRIDE
PeptideAtlas
MassIVE
JPOST Repository
Physiome Model Repository

EGA
EVA
ENA
LINCS
PAXDB
Cell Collective

MetaboLights
Metabolomics Workbench
MetabolomeExpress
GNPS
BioModels
FAIRDOMHub

ArrayExpress
dbGaP
ExpressionAtlas
GEO
NODE

Information

Databases
Help
API
Contact us
Code on GitHub
Terms of use
Submit Data