Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1803.03092

Carnap: An Open Framework for Formal Reasoning in the Browser

Graham Leach-Krouse
View original source ↗Read source document ↗Export metadata ↓

Abstract

This paper presents an overview of Carnap, a free and open framework for the development of formal reasoning applications. Carnap's design emphasizes flexibility, extensibility, and rapid prototyping. Carnap-based applications are written in Haskell, but can be compiled to JavaScript to run in standard web browsers. This combination of features makes Carnap ideally suited for educational applications, where ease-of-use is crucial for students and adaptability to different teaching strategies and classroom needs is crucial for instructors. The paper describes Carnap's implementation, along with its current and projected pedagogical applications.

Explore related subjects

cs.HC

Keep this discovery

BibTeXRIS

Graham Leach-Krouse. 2018-03-05. Carnap: An Open Framework for Formal Reasoning in the Browser. https://doi.org/10.4204/eptcs.267.5

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

ShellVis: Sandboxed Live Programming for Shell Scripts

Live programming provides visibility to programmers by running and tracing programs as they are edited. However, for programs with potentially harmful side effects, liveness can turn mistakes into disasters. We propose enabling live programming in environments with side effects via sandboxing: confining effects to a simulation of the true environment. We apply sandboxed live programming in the challenging context of shell scripting: a ubiquitous and powerful---yet notoriously opaque and error-prone---tool. ShellVis provides line-by-line feedback on a shell script's run-time behavior, with file operations sandboxed via a safe overlay of the file system. A qualitative user evaluation finds ShellVis to be helpful to participants, replacing tedious existing practices and instilling confidence. Participant responses also reveal areas for future research, particularly bridging the gulf of execution alongside the gulf of evaluation. ShellVis serves as a case study of how sandboxing can bring live-programming techniques into the many real-world programming contexts where side effects are important.

cs.HC↗
arXiv2026

Visual-Motion-Induced Modulation of Pedestrian Trajectories Using Spatially Distributed Multi-Display Signage in Public Spaces

Multi-display signage (MDS), now ubiquitous in urban environments, has the potential to influence human behavior and experience in public spaces. However, despite its unique capability to present spatially distributed dynamic visual stimuli, its current use is mainly limited to advertising. In this study, we propose a perception-based approach for laterally modulating pedestrian trajectories as a nonverbal means of guiding pedestrians in public spaces. The approach is motivated by vection, the illusion of self-motion, and uses laterally moving monochrome stripes, a standard stimulus in vection research, presented across spatially distributed displays to elicit postural responses that may bias pedestrian trajectories. We evaluated the approach through a controlled laboratory experiment and a real-world field deployment involving actual pedestrian flows in a national museum. The laboratory experiment examined whether the MDS setup induced trajectory shifts in the direction predicted by prior research on the behavioral effects of vection. The field deployment investigated whether comparable effects would emerge in aggregate pedestrian behavior during unconstrained movement under conditions closer to those of urban public spaces. In the laboratory, full-screen motion significantly biased walking trajectories in the direction of visual motion, whereas partial-stripe motion produced no significant directional effect. In the field deployment, opposing full-screen motion conditions produced direction-consistent differences in aggregate pedestrian positions. The field results, observed despite the substantial variability in real-world pedestrian flows, extend the controlled laboratory findings and provide ecologically valid evidence supporting practical MDS-based pedestrian modulation in public settings. The results further suggest that sufficient visual-motion coverage may be important.

cs.HC↗
arXiv2026

How AI Coders Discuss, Disagree, and Reach Consensus: Challenges and Opportunities for LLM-Based Qualitative Coding

The utility of AI in multi-coder qualitative coding has been widely discussed, yet little empirical evidence exists to delineate the contexts in which it performs reliably. We address this gap by quantifying the effectiveness of multi-agent LLM coding across varied qualitative datasets, revealing key contextual and structural factors that mediate coding outcomes. We developed a literature-informed baseline pipeline that enables AI agents to independently code, debate, and reconcile disagreements. Results revealed that coding accuracy depends on factors such as codebook length, qualitative data similarity, and agent disagreement. Notably, intense and unresolved debates between agents led to higher accuracy. Our analysis showed that while LLMs emulate many human discussion behaviors, they lack adaptive responsiveness to context. From these findings, we offer design recommendations for building automated coding systems. Our open-source AI discussion dataset and methodological framework lay the groundwork for advancing the design of AI-mediated automated thematic analysis.

cs.HC↗