High School Is this equation at all sensical?

Click For Summary
SUMMARY

The equation ∀t(T(x,t)⟹(¬H(x,t)∨H(x,t+Δt))) lacks context and specificity, rendering it largely useless without defined variables. It suggests a logical relationship where T(x,t) is false if H(x,t) is true, indicating a transition in H over time. The discussion hints at its potential origins in formal hardware description languages (HDLs) or theorem proving contexts, particularly referencing the Boyer-Moore Theorem Prover and ACL2, a programming language for modeling computer systems.

PREREQUISITES
  • Understanding of logical operators and their implications in mathematical expressions.
  • Familiarity with time variables in mathematical modeling, specifically Δt.
  • Knowledge of formal hardware description languages (HDLs).
  • Experience with theorem proving tools, particularly ACL2.
NEXT STEPS
  • Research the Boyer-Moore Theorem Prover and its applications in formal verification.
  • Explore ACL2 and its capabilities for modeling and proving properties of computer systems.
  • Learn about formal HDLs and their role in describing logic functions.
  • Investigate the implications of logical transitions in time-based systems.
USEFUL FOR

This discussion is beneficial for mathematicians, computer scientists, and engineers involved in formal verification, theorem proving, and those working with hardware description languages.

DaveC426913
Gold Member
Messages
24,140
Reaction score
8,264
TL;DR
This looks like nonsense, or at least nothing meaningful.
(Yes, I'm guilty of passing along something incomplete and of utterly unknown provenance that someone saw somewhere and didn't understand. I feel dirty.)


∀t(T(x,t)⟹(¬H(x,t)∨H(x,t+Δt)))

Certainly, without specifying any of the variables, it's got to be useless. At least we can assume t and Δt refer to time/delta time - which is my rationale for posting here in the physics subforum)

Chat GPT made a broad guess but couldn't make heads or tails of it either. Don't judge me.
 
Physics news on Phys.org
I would normally interpret those symbols as logical operators, so you might be better asking in the relevant maths forum. Difficult to tell without context, though.
 
∀t(T(x,t)⟹(¬H(x,t)∨H(x,t+Δt)))
For all t, T(x,t) implies ( NOT( H(x,t) ) OR H(x,t+Δt) )
T(x,t) is FALSE if H(x,t) was TRUE, and H(x,t+Δt) is FALSE.
T(x,t) is FALSE when H(x,t) transitions to FALSE in next sample.
A negative edge in H causes T to go low for one cycle.

Maybe it is from a formal HDL used to describe logic functions.
 
  • Like
Likes SammyS, Ibix and PeroK
It looks a bit like input code for a Boyer-Moore Theorem Prover.
Example here: https://en.wikipedia.org/wiki/Nqthm#Theorem_formulation
"(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z))"

ACL2 or "A Computational Logic for Applicative Common Lisp", an applicative (side-effect free) variant of Common LISP. ACL2 is both a programming language which can model computer systems, and a tool to help proving properties of those models.
 

Similar threads

  • · Replies 4 ·
Replies
4
Views
4K
  • · Replies 13 ·
Replies
13
Views
21K
Replies
2
Views
4K
  • · Replies 5 ·
Replies
5
Views
2K
  • · Replies 7 ·
Replies
7
Views
2K
  • · Replies 10 ·
Replies
10
Views
2K
  • · Replies 4 ·
Replies
4
Views
2K
  • · Replies 5 ·
Replies
5
Views
1K
  • · Replies 7 ·
Replies
7
Views
1K
Replies
1
Views
2K